aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintAsm.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2018-03-06 09:59:23 +0100
committerGitHub <noreply@github.com>2018-03-06 09:59:23 +0100
commit7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f (patch)
tree550a1a180c7296a125f6f8e5813460e2c078127b /backend/PrintAsm.ml
parent086c6686ec93cdaf7b6433cffdc4d8403a06f8b6 (diff)
downloadcompcert-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 'backend/PrintAsm.ml')
-rw-r--r--backend/PrintAsm.ml24
1 files changed, 14 insertions, 10 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 44c6b409..04ecbae3 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -18,6 +18,7 @@ open PrintAsmaux
open Printf
open Sections
open TargetPrinter
+open AisAnnot
module Printer(Target:TARGET) =
struct
@@ -148,21 +149,24 @@ module Printer(Target:TARGET) =
| Gvar v -> print_var oc name v
let print_ais_annot oc =
- let annots = List.rev !ais_annot_list in
+ let annots = get_ais_annots () in
if annots <> [] then begin
Target.section oc Section_ais_annotation;
- let annot_part oc lbl = function
- | Str.Delim _ ->
- fprintf oc " .byte 7,%d\n" (if Archi.ptr64 then 8 else 4) ;
- fprintf oc " %s %a\n" Target.address Target.label lbl
- | Str.Text a -> fprintf oc " .ascii %S\n" a in
- let annot oc (lbl,str) =
- List.iter (annot_part oc lbl) str;
+ let print_addr oc pp_addr addr =
+ fprintf oc " .byte 7,%d\n" (if Archi.ptr64 then 8 else 4);
+ fprintf oc " %s %a\n" Target.address pp_addr addr in
+ let annot_part oc = function
+ | AisAnnot.Label lbl ->
+ print_addr oc Target.label lbl
+ | AisAnnot.Symbol symb ->
+ print_addr oc Target.symbol symb
+ | AisAnnot.String a -> fprintf oc " .ascii %S\n" a in
+ let annot oc str =
+ List.iter (annot_part oc) str;
fprintf oc " .ascii \"\\n\"\n"
in
List.iter (annot oc) annots
- end;
- ais_annot_list := []
+ end
module DwarfTarget: DwarfTypes.DWARF_TARGET =
struct