New support for inserting ais-annotations.

The ais annotations can be inserted via the new ais variants of
the builtin annotation. They mainly differe in that they have an
address format specifier '%addr' which will be replaced by the
adress in the binary.

The implementation simply prints a label for the builtin call
alongside a the text of the annotation as comment and inserts the
annotation together as acii string in a separate section
'ais_annotations' and replaces the usages of the address format
specifiers by the address of the label of the builtin call.

1 files changed, 10 insertions, 0 deletions

diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index df3445ea..07ab4bed 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -197,6 +197,16 @@ let annot_text preg_string sp_reg_name txt args =
         sprintf "<bad parameter %s>" s in
   String.concat "" (List.map fragment (Str.full_split re_annot_param txt))
 
+let ais_annot_list: (int * Str.split_result list) list ref = ref []
+
+let re_annot_addr = Str.regexp "%addr"
+
+let ais_annot_text lbl preg_string sp_reg_name txt args =
+  let annot = annot_text preg_string sp_reg_name txt args in
+  let annots = Str.full_split re_annot_addr annot in
+  ais_annot_list := (lbl,annots)::!ais_annot_list;
+  annot
+
 (* Printing of [EF_debug] info.  To be completed. *)
 
 let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"