diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-03-06 09:59:23 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-06 09:59:23 +0100 |
| commit | 7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f (patch) | |
| tree | 550a1a180c7296a125f6f8e5813460e2c078127b /arm/TargetPrinter.ml | |
| parent | 086c6686ec93cdaf7b6433cffdc4d8403a06f8b6 (diff) | |
| download | compcert-kvx-7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f.tar.gz compcert-kvx-7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f.zip | |
Reactivated and improved ais annotations.
The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.
Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.
Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.
Diffstat (limited to 'arm/TargetPrinter.ml')
| -rw-r--r-- | arm/TargetPrinter.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 56619cdd..9c1e296b 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -15,6 +15,7 @@ open Printf open Camlcoq open Sections +open AisAnnot open AST open Asm open PrintAsmaux @@ -459,15 +460,15 @@ struct | Pbuiltin(ef, args, res) -> begin match ef with | EF_annot(kind,txt, targs) -> - let annot = begin match (P.to_int kind) with - | 1 -> annot_text preg_annot "sp" (camlstring_of_coqstring txt) args + | 1 -> let annot = annot_text preg_annot "sp" (camlstring_of_coqstring txt) args in + fprintf oc "%s annotation: %S\n" comment annot | 2 -> let lbl = new_label () in fprintf oc "%a: " label lbl; - ais_annot_text lbl preg_annot "sp" (camlstring_of_coqstring txt) args + add_ais_annot lbl preg_annot "sp" (camlstring_of_coqstring txt) args | _ -> assert false - end in - fprintf oc "%s annotation: %S\n" comment annot + end; + 0 | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "sp" oc (P.to_int kind) (extern_atom txt) args |