aboutsummaryrefslogtreecommitdiffstats
path: root/arm/TargetPrinter.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2017-08-17 11:26:22 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2017-08-17 11:26:22 +0200
commit6c34468898e3726b53c875023730fae7caaf88ee (patch)
tree4c179bd1514b6c1168f2c5fa0132e4e85e898ce2 /arm/TargetPrinter.ml
parent82c4547961d567003a83d6c489e06f1271e80a7f (diff)
downloadcompcert-kvx-6c34468898e3726b53c875023730fae7caaf88ee.tar.gz
compcert-kvx-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 'arm/TargetPrinter.ml')
-rw-r--r--arm/TargetPrinter.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 02c348a8..1dfe8af6 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -693,8 +693,6 @@ struct
assert false
| Pfreeframe(sz, ofs) ->
assert false
- | Psavelr(ofs) ->
- assert false
| Plabel lbl ->
fprintf oc "%a:\n" print_label lbl; 0
| Ploadsymbol(r1, id, ofs) ->