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.

1 files changed, 0 insertions, 12 deletions

diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index d985d5a4..f9ed569f 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -212,18 +212,6 @@ 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 re_annot_quote = Str.regexp "\007"
-
-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 annot = Str.global_replace re_annot_quote "\007\000" annot 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]*\\)$"