tree 7a0b60fc95847b5876abc126009f49f784d3e7c9
parent 37402879072a5d320bb6d0642b02836ce486da64
author Wedson Almeida Filho <wedsonaf@google.com> 1539086421 +0100
committer Wedson Almeida Filho <wedsonaf@google.com> 1540391874 +0100

Update assembly code to simplify verification.

1. Use sub & cbnz instead of subs & b.ne, so that we don't have to model
the flags.
2. Always use the callstack explicitly, that is, always subtract from sp
before writing data.
3. Remove two instructions from the vcpu_switch path.

Change-Id: I04e05736e112ffc6b3c475ad79559069d8a0f4fd