diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-01 15:32:13 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-01 15:32:13 +0000 |
commit | 5020a5a07da3fd690f5d171a48d0c73ef48f9430 (patch) | |
tree | 3ddd75a3ef65543de814f2e0881f8467df73e089 /arm/PrintAsm.ml | |
parent | f401437a97b09726d029e3a1b65143f34baaea70 (diff) | |
download | compcert-5020a5a07da3fd690f5d171a48d0c73ef48f9430.tar.gz compcert-5020a5a07da3fd690f5d171a48d0c73ef48f9430.zip |
Revised Stacking and Asmgen passes and Mach semantics:
- no more prediction of return addresses (Asmgenretaddr is gone)
- instead, punch a hole for the retaddr in Mach stack frame and
fill this hole with the return address in the Asmgen proof.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/PrintAsm.ml')
-rw-r--r-- | arm/PrintAsm.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 278b6b18..f5b04b54 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -593,14 +593,14 @@ let print_instruction oc = function fprintf oc " fsts %a, [%a, #%a]\n" freg_single FR6 ireg r2 coqint n; 2 (* Pseudo-instructions *) | Pallocframe(sz, ofs) -> - fprintf oc " mov r12, sp\n"; + fprintf oc " mov r10, sp\n"; let ninstr = ref 0 in List.iter (fun n -> fprintf oc " sub sp, sp, #%a\n" coqint n; incr ninstr) (Asmgen.decompose_int sz); - fprintf oc " str r12, [sp, #%a]\n" coqint ofs; + fprintf oc " str r10, [sp, #%a]\n" coqint ofs; 2 + !ninstr | Pfreeframe(sz, ofs) -> if Asmgen.is_immed_arith sz @@ -614,7 +614,8 @@ let print_instruction oc = function fprintf oc " ldr %a, .L%d @ %a\n" ireg r1 lbl print_symb_ofs (id, ofs); 1 | Pbtbl(r, tbl) -> - fprintf oc " ldr pc, [pc, %a]\n" ireg r; + fprintf oc " mov r14, %a, lsl #2\n"; + fprintf oc " ldr pc, [pc, r14]\n"; fprintf oc " mov r0, r0\n"; (* no-op *) List.iter (fun l -> fprintf oc " .word %a\n" print_label l) |