diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-17 11:26:22 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-17 11:26:22 +0200 |
commit | 6c34468898e3726b53c875023730fae7caaf88ee (patch) | |
tree | 4c179bd1514b6c1168f2c5fa0132e4e85e898ce2 /cfrontend/Clight.v | |
parent | 82c4547961d567003a83d6c489e06f1271e80a7f (diff) | |
download | compcert-6c34468898e3726b53c875023730fae7caaf88ee.tar.gz compcert-6c34468898e3726b53c875023730fae7caaf88ee.zip |
ARM port: replace Psavelr pseudo-instruction by actual instructions
Saving the return address register (R14) in the function prologue can be done either with a single "str" instruction if the offset is small enough, or by constructing the address using the R12 register as a temporary then storing with "str" relative to R12.
R12 can be used as a temporary because it is marked as destroyed at function entry. We just need to tell Asmgen.translcode whether R12 still contains the back link left there by Pallocframe, or R12 was trashed. In the latter case R12 will be reloaded from the stack at the next Mgetparam instruction.
Diffstat (limited to 'cfrontend/Clight.v')
0 files changed, 0 insertions, 0 deletions