diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-06 19:38:53 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-06 19:38:53 +0200 |
| commit | dba05a9f6259c82a350987b511bf1a71f113d0ba (patch) | |
| tree | 6e7fee8d65b6a180447267da9a95a93827443caf /arm/TargetPrinter.ml | |
| parent | 108db39b8b7c1d42cbc38c5aabf885ef5440f189 (diff) | |
| parent | 47d0e5256ab79b402faae14260fa2fabc1d24dcb (diff) | |
| download | compcert-kvx-dba05a9f6259c82a350987b511bf1a71f113d0ba.tar.gz compcert-kvx-dba05a9f6259c82a350987b511bf1a71f113d0ba.zip | |
X
Merge branch 'master' into debug_locations
Diffstat (limited to 'arm/TargetPrinter.ml')
| -rw-r--r-- | arm/TargetPrinter.ml | 32 |
1 files changed, 11 insertions, 21 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 33071a9a..028ff6ed 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -305,17 +305,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) -(* Handling of annotations *) - - let print_annot_stmt oc txt targs args = - if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) - (int_of_string (Str.matched_group 2 txt)) - end else begin - fprintf oc "%s annotation: " comment; - print_annot_stmt preg "sp" oc txt targs args - end - (* Auxiliary for 64-bit integer arithmetic built-ins. They expand to two instructions, one computing the low 32 bits of the result, followed by another computing the high 32 bits. In cases where @@ -521,7 +510,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " bic%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 | Pclz (r1,r2) -> - fprintf oc " clz %a, %a\n" preg r1 preg r2; 1 + fprintf oc " clz %a, %a\n" ireg r1 ireg r2; 1 | Pcmp(r1, so) -> fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1 | Pdmb -> @@ -571,9 +560,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " orr%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 | Prev (r1,r2) -> - fprintf oc " rev %a, %a\n" preg r1 preg r2; 1 + fprintf oc " rev %a, %a\n" ireg r1 ireg r2; 1 | Prev16 (r1,r2) -> - fprintf oc " rev16 %a, %a\n" preg r1 preg r2; 1 + fprintf oc " rev16 %a, %a\n" ireg r1 ireg r2; 1 | Prsb(r1, r2, so) -> fprintf oc " rsb%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 @@ -782,6 +771,14 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end | Pbuiltin(ef, args, res) -> begin match ef with + | EF_annot(txt, targs) -> + fprintf oc "%s annotation: " comment; + print_annot_text preg "sp" oc (extern_atom txt) args; + 0 + | EF_debug(kind, txt, targs) -> + print_debug_info comment print_file_line preg "sp" oc + (P.to_int kind) (extern_atom txt) args; + 0 | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg oc (extern_atom txt) sg args res; @@ -790,13 +787,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | _ -> assert false end - | Pannot(ef, args) -> - begin match ef with - | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args; 0 - | _ -> - assert false - end | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0 let no_fallthrough = function |