diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-14 22:41:44 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-14 22:41:44 +0200 |
| commit | cfdf756faa342378b7befd78d8288213f76c86e1 (patch) | |
| tree | 66c01ede95a5bcfc84eadbc2408cec1359ae7f2f /arm/TargetPrinter.ml | |
| parent | 4c146156a36d48209a6206f61f80dc5d4c48ce93 (diff) | |
| download | compcert-cfdf756faa342378b7befd78d8288213f76c86e1.tar.gz compcert-cfdf756faa342378b7befd78d8288213f76c86e1.zip | |
Updated the branch and implemented the suggested changes.
Diffstat (limited to 'arm/TargetPrinter.ml')
| -rw-r--r-- | arm/TargetPrinter.ml | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 88261940..f8d72836 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -539,6 +539,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " ldrb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Pldrh(r1, r2, sa) -> fprintf oc " ldrh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldr_p(r1, r2, sa) -> + fprintf oc " ldr %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldrb_p(r1, r2, sa) -> + fprintf oc " ldrb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldrh_p(r1, r2, sa) -> + fprintf oc " ldrh %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 | Pldrsb(r1, r2, sa) -> fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Pldrsh(r1, r2, sa) -> @@ -591,6 +597,17 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " strb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Pstrh(r1, r2, sa) -> fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Pstr_p(r1, r2, sa) -> + fprintf oc " str %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; + begin match r1, r2, sa with + | IR14, IR13, SOimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n) + | _ -> () + end; + 1 + | Pstrb_p(r1, r2, sa) -> + fprintf oc " strb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + | Pstrh_p(r1, r2, sa) -> + fprintf oc " strh %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 | Psdiv -> if Opt.hardware_idiv then begin fprintf oc " sdiv r0, r0, r1\n"; 1 |