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.

15 files changed, 289 insertions, 73 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
diff --git a/backend/AisAnnot.ml b/backend/AisAnnot.ml
new file mode 100644
index 00000000..f4dab4c9
--- /dev/null
+++ b/backend/AisAnnot.ml
@@ -0,0 +1,159 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open AST
+open Camlcoq
+open Diagnostics
+open Memdata
+open Printf
+
+type t =
+  | Label of int
+  | String of string
+  | Symbol of ident
+
+let offset ofs =
+  let ofs = camlint_of_coqint ofs in
+  if ofs = 0l then "" else sprintf " + %ld" ofs
+
+let size_chunk c =
+  sprintf "%ld" (camlint_of_coqint (size_chunk c))
+
+let addr_global id ofs =
+  let addr_o = "("
+  and addr_e = sprintf "%s)" (offset ofs) in
+  [String addr_o;Symbol id;String addr_e]
+
+exception Bad_parameter of string
+exception Unknown_parameter of string
+exception Unknown_type of char
+
+let ais_expr_arg lval preg_string sp_reg_name arg =
+  let preg reg = sprintf "reg(\"%s\")" (preg_string reg)
+  and sp = sprintf "reg(\"%s\")" sp_reg_name
+  and simple s = [String s]
+  and lval ty =
+    if lval then
+      let msg = sprintf "expected register or memory cell but found %s" ty in
+      raise (Bad_parameter msg)
+  in
+  let rec ais_arg = function
+  | BA x -> simple (preg x)
+  | BA_int n -> lval "constant"; simple (sprintf "%ld" (camlint_of_coqint n))
+  | BA_long n ->lval "constant"; simple (sprintf "%Ld" (camlint64_of_coqint n))
+  | BA_float _
+  | BA_single _ -> assert false (* Should never occur and be avoided in C2C *)
+  | BA_loadstack(chunk, ofs) ->
+    let loadstack = sprintf "mem(%s%s, %s)" sp
+                       (offset ofs)
+                       (size_chunk chunk) in
+    simple loadstack
+  | BA_addrstack ofs ->
+    lval "stack cell";
+    let addrstack  = sprintf "(%s%s)" sp (offset ofs) in
+    simple addrstack
+  | BA_loadglobal(chunk, id, ofs) ->
+    let mem_o = "mem("
+    and mem_e = sprintf "%s, %s)"
+        (offset ofs)
+        (size_chunk chunk) in
+    [String mem_o;Symbol id;String mem_e]
+  | BA_addrglobal(id, ofs) ->
+    lval "global address";
+    addr_global id ofs
+  | BA_splitlong(hi, lo) ->
+    combine " * 0x100000000 + " hi lo
+  | BA_addptr(a1, a2) ->
+    combine " + " a1 a2
+  and combine mid arg1 arg2 =
+    lval "pointer computation";
+    let op_br = simple "("
+    and mid = simple mid
+    and cl_br = simple ")"
+    and arg1 = ais_arg arg1
+    and arg2 = ais_arg arg2 in
+    op_br@arg1@mid@arg2@cl_br in
+  ais_arg arg
+
+let ais_annot_list: (t list) list ref = ref []
+
+let get_ais_annots () =
+  let annots = !ais_annot_list in
+  ais_annot_list := [];
+  List.rev annots
+
+let re_loc_param = Str.regexp "# file:\\([^ ]+\\) line:\\([^ ]+\\)"
+
+let loc_of_txt txt =
+  try
+    let pos = String.index txt '\n' in
+    let txt = String.sub txt 0 (pos -1) in
+    if Str.string_partial_match re_loc_param txt 0 then
+      let file = Str.matched_group 1 txt
+      and line = int_of_string (Str.matched_group 2 txt) in
+      file,line
+    else
+      no_loc
+  with _ ->
+    no_loc
+
+let re_ais_annot_param = Str.regexp "%%\\|%[aelp][1-9][0-9]*\\|%here\\|\007"
+
+let add_ais_annot lbl preg_string sp_reg_name txt args =
+  let fragment = function
+    | Str.Delim "%here" ->
+      [Label lbl]
+    | Str.Text s ->
+      [String s]
+    | Str.Delim "%%" ->
+      [String "%"]
+    | Str.Delim "\007" ->
+      [String "\007\000"]
+    | Str.Delim s ->
+      let typ = String.get s 1
+      and n = int_of_string (String.sub s 2 (String.length s - 2)) in
+      let arg = try
+          List.nth args (n-1)
+        with _ ->
+           raise (Unknown_parameter s) in
+      begin match typ with
+        | 'e' -> ais_expr_arg false preg_string sp_reg_name arg
+        | 'l' -> ais_expr_arg true preg_string sp_reg_name arg
+        | _ -> raise (Unknown_type typ)
+      end
+  in
+  let loc = loc_of_txt txt in
+  let warn t s =
+    warning loc Wrong_ais_parameter "%s %s" t s; []
+  in
+  let annot  =
+    try
+      List.concat (List.map fragment (Str.full_split re_ais_annot_param txt))
+    with
+    | Bad_parameter s ->
+      warn "wrong ais parameter" s
+    | Unknown_parameter s ->
+      warn "unknown parameter" s
+    | Unknown_type c ->
+      warn "unknown format argument" (String.make 1 c)
+  in
+  let rec merge acc = function
+    | [] -> List.rev acc
+    | (Label _ as lbl):: rest ->  merge (lbl::acc) rest
+    | (Symbol _ as sym) :: rest -> merge (sym::acc) rest
+    | String s1 :: String s2 :: rest ->
+      merge acc (String (s1 ^ s2) :: rest)
+    | String s:: rest  ->  merge ((String s)::acc) rest
+  in
+  let annot = merge [] annot in
+  if annot <> [] then
+    ais_annot_list := (annot)::!ais_annot_list
diff --git a/backend/AisAnnot.mli b/backend/AisAnnot.mli
new file mode 100644
index 00000000..7219369c
--- /dev/null
+++ b/backend/AisAnnot.mli
@@ -0,0 +1,31 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+type t =
+  | Label of int        (** label argument, used for current location*)
+  | String of string    (** text part of the ais annotation *)
+  | Symbol of AST.ident (** symbol argument, used in variable and function addresses *)
+
+val add_ais_annot : int -> ('a -> string) -> string -> string -> 'a AST.builtin_arg list -> unit
+(** [add_ais_annot lbl preg spreg txt args] adds the ais annotation [txt] were the format
+    specifiers are replace according to their type:
+    -a: area definitions
+    -e: general expressions
+    -l: l-value expressions
+    -p: program location
+    -here: the address of the ais annotation [lbl]
+    and [preg] is used to get the names of the registers, as well as [spreg] the name of the
+    stack pointer and [args] the arguments reference in the replacements
+*)
+
+val get_ais_annots: unit -> (t list) list
+(** [get_ais_annots ()] return the list of all ais annotations and reset it *)
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
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]*\\)$"
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index b8134599..c18a6e03 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -119,6 +119,10 @@ let currentLocation = ref Cutil.no_loc
 
 let updateLoc l = currentLocation := l
 
+let currentFunction = ref ""
+
+let updateFunction f = currentFunction := f
+
 let error fmt =
   Diagnostics.error !currentLocation fmt
 
@@ -140,21 +144,21 @@ let string_of_errmsg msg =
 
 (** ** The builtin environment *)
 
-(* let ais_annot_functions =
- *   if Configuration.elf_target then
- *     [(\* Ais Annotations, only available for ELF targets *\)
- *       "__builtin_ais_annot",
- *       (TVoid [],
- *        [TPtr(TInt(IChar, [AConst]), [])],
- *        true);]
- *   else
- *     [] *)
+let ais_annot_functions =
+  if Configuration.elf_target then
+    [(* Ais Annotations, only available for ELF targets *)
+       "__builtin_ais_annot",
+     (TVoid [],
+      [TPtr(TInt(IChar, [AConst]), [])],
+      true);]
+  else
+    []
 
 let builtins_generic = {
   Builtins.typedefs = [];
   Builtins.functions =
-    (* ais_annot_functions
-     * @ *)
+    ais_annot_functions
+      @
     [
     (* Integer arithmetic *)
     "__builtin_bswap",
@@ -871,19 +875,25 @@ let rec convertExpr env e =
           ezero
       end
 
-  (* | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot"}}, args) when Configuration.elf_target ->
-   *     begin match args with
-   *     | {edesc = C.EConst(CStr txt)} :: args1 ->
-   *       let file,line = !currentLocation in
-   *       let loc_string = Printf.sprintf "# file %s, line %d\n" file line in
-   *       let targs1 = convertTypArgs env [] args1 in
-   *         Ebuiltin(
-   *            AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ txt), typlist_of_typelist targs1),
-   *           targs1, convertExprList env args1, convertTyp env e.etyp)
-   *     | _ ->
-   *         error "argument 1 of '__builtin_ais_annot' must be a string literal";
-   *         ezero
-   *     end *)
+  | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot"}}, args) when Configuration.elf_target ->
+      begin match args with
+      | {edesc = C.EConst(CStr txt)} :: args1 ->
+        let file,line = !currentLocation in
+        let fun_name = !currentFunction in
+        let loc_string = Printf.sprintf "# file:%s line:%d function:%s\n" file line fun_name in
+        let targs1 = convertTypArgs env [] args1 in
+        List.iter (fun exp -> if Cutil.is_float_type env exp.etyp then begin
+            error "floating point types are not supported in ais annotations"
+          end else if Cutil.is_volatile_variable env exp then begin
+            error "access to volatile variables are not supported in ais annotations"
+          end) args1;
+          Ebuiltin(
+             AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ txt), typlist_of_typelist targs1),
+            targs1, convertExprList env args1, convertTyp env e.etyp)
+      | _ ->
+          error "argument 1 of '__builtin_ais_annot' must be a string literal";
+          ezero
+      end
 
  | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) ->
       make_builtin_memcpy (convertExprList env args)
@@ -1135,6 +1145,7 @@ and convertSwitch env is_64 = function
 
 let convertFundef loc env fd =
   checkFunctionType env fd.fd_ret (Some fd.fd_params);
+  updateFunction fd.fd_name.name;
   if fd.fd_vararg && not !Clflags.option_fvararg_calls then
     unsupported "variable-argument function (consider adding option [-fvararg-calls])";
   let ret =
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 71c253f8..30037049 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -707,6 +707,11 @@ let is_integer_type env t =
   | TEnum(_, _) -> true
   | _ -> false
 
+let is_float_type env t =
+  match unroll env t with
+  | TFloat (_, _) -> true
+  | _ -> false
+
 let is_arith_type env t =
   match unroll env t with
   | TInt(_, _) -> true
@@ -1207,3 +1212,8 @@ let rec subst_stmt phi s =
                List.map subst_asm_operand inputs,
                clob)
   }
+
+let is_volatile_variable env exp =
+  match exp.edesc with
+  |  EVar x -> List.mem AVolatile (attributes_of_type env exp.etyp)
+  | _ -> false
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 79975dcf..87a69f12 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -141,6 +141,8 @@ val is_void_type : Env.t -> typ -> bool
   (* Is type [void]? *)
 val is_integer_type : Env.t -> typ -> bool
   (* Is type integer? *)
+val is_float_type : Env.t -> typ -> bool
+  (* Is type float *)
 val is_arith_type : Env.t -> typ -> bool
   (* Is type integer or float? *)
 val is_pointer_type : Env.t -> typ -> bool
@@ -239,6 +241,8 @@ val field_of_arrow_access: Env.t -> typ -> string -> field
   (* Return the field info for a [x->field] access *)
 val valid_array_size: Env.t -> typ -> int64 -> bool
   (* Test whether the array size fits in half of the address space *)
+val is_volatile_variable: Env.t -> exp -> bool
+  (* Test whether the expression is an access to a volatile variable *)
 
 (* Constructors *)
 
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml
index fbdc9297..e3258a38 100644
--- a/cparser/Diagnostics.ml
+++ b/cparser/Diagnostics.ml
@@ -90,6 +90,7 @@ type warning_type =
   | Inline_asm_sdump
   | Unused_variable
   | Unused_parameter
+  | Wrong_ais_parameter
 
 (* List of active warnings *)
 let active_warnings: warning_type list ref = ref [
@@ -110,6 +111,7 @@ let active_warnings: warning_type list ref = ref [
   Return_type;
   Literal_range;
   Inline_asm_sdump;
+  Wrong_ais_parameter;
 ]
 
 (* List of errors treated as warning *)
@@ -139,6 +141,7 @@ let string_of_warning = function
   | Inline_asm_sdump -> "inline-asm-sdump"
   | Unused_variable -> "unused-variable"
   | Unused_parameter -> "unused-parameter"
+  | Wrong_ais_parameter -> "wrong-ais-parameter"
 
 (* Activate the given warning *)
 let activate_warning w () =
@@ -184,7 +187,8 @@ let wall () =
     CompCert_conformance;
     Inline_asm_sdump;
     Unused_variable;
-    Unused_parameter
+    Unused_parameter;
+    Wrong_ais_parameter;
   ]
 
 let wnothing () =
@@ -214,6 +218,7 @@ let werror () =
     CompCert_conformance;
     Inline_asm_sdump;
     Unused_variable;
+    Wrong_ais_parameter;
   ]
 
 (* Generate the warning key for the message *)
@@ -390,6 +395,7 @@ let warning_options =
   error_option Inline_asm_sdump @
   error_option Unused_variable @
   error_option Unused_parameter @
+  error_option Wrong_ais_parameter @
   [Exact ("-Wfatal-errors"), Set error_fatal;
    Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *)
    Exact ("-fno-diagnostics-color"), Unset color_diagnostics;
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli
index 82edd9fa..648d537b 100644
--- a/cparser/Diagnostics.mli
+++ b/cparser/Diagnostics.mli
@@ -47,6 +47,7 @@ type warning_type =
   | Inline_asm_sdump               (** inline assembler used in combination of sdump *)
   | Unused_variable                (** unused local variables *)
   | Unused_parameter               (** unused function parameter *)
+  | Wrong_ais_parameter            (** wrong parameter type for ais replacement *)
 
 val warning  : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a
 (** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 8143954b..b2c83698 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -69,7 +69,7 @@ let preprocessed_file transfs name sourcefile =
              | Parser.Parser.Inter.Fail_pr ->
                  (* Theoretically impossible : implies inconsistencies
                     between grammars. *)
-                 Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing"
+               Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing"
              | Parser.Parser.Inter.Timeout_pr -> assert false
              | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in
       let p1 = Timing.time "Elaboration" Elab.elab_file ast in
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index cdb5751e..d63fa47d 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -84,7 +84,7 @@ let ident env id =
     IdentMap.find id env.re_id
   with Not_found ->
     Diagnostics.fatal_error Diagnostics.no_loc "internal error: rename: %s__%d unbound"
-                        id.name id.stamp
+      id.name id.stamp
 
 let rec typ env = function
   | TPtr(ty, a) -> TPtr(typ env ty, a)
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 01851ac2..9a6840b1 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -20,6 +20,7 @@ open Sections
 open AST
 open Asm
 open PrintAsmaux
+open AisAnnot
 
 (* Recognition of target ABI and asm syntax *)
 
@@ -834,15 +835,15 @@ module Target (System : SYSTEM):TARGET =
       | 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
-                | 2 -> let lbl = new_label () in
-                  fprintf oc "%a: " label lbl;
-                  ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args
-                | _ -> assert false
-              end in
-            fprintf oc "%s annotation: %S\n" comment annot
+            begin match (P.to_int kind) with
+              | 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;
+                add_ais_annot lbl preg_annot "r1" (camlstring_of_coqstring txt) args
+              | _ -> assert false
+              end
           | EF_debug(kind, txt, targs) ->
               print_debug_info comment print_file_line preg_annot "r1" oc
                                (P.to_int kind) (extern_atom txt) args
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 696bc87f..381f4397 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -22,6 +22,7 @@ open Camlcoq
 open Sections
 open AST
 open Asm
+open AisAnnot
 open PrintAsmaux
 open Fileinfo
 
@@ -566,15 +567,14 @@ module Target : TARGET =
       | 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 "r1" (camlstring_of_coqstring txt) args
+                 add_ais_annot lbl preg_annot "r1" (camlstring_of_coqstring txt) args
                | _ -> assert false
-             end in
-             fprintf oc "%s annotation: %S\n" comment annot
+             end
           | EF_debug(kind, txt, targs) ->
               print_debug_info comment print_file_line preg_annot "sp" oc
                                (P.to_int kind) (extern_atom txt) args
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 3171847c..12ef6472 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -17,6 +17,7 @@ open Camlcoq
 open Sections
 open AST
 open Asm
+open AisAnnot
 open PrintAsmaux
 open Fileinfo
 
@@ -792,15 +793,14 @@ module Target(System: SYSTEM):TARGET =
       | 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 "r1" (camlstring_of_coqstring txt) args
+                    add_ais_annot lbl preg_annot "r1" (camlstring_of_coqstring txt) args
                   | _ -> assert false
-                end in
-              fprintf oc "%s annotation: %S\n" comment annot
+                end
           | EF_debug(kind, txt, targs) ->
               print_debug_info comment print_file_line preg_annot "%esp" oc
                                (P.to_int kind) (extern_atom txt) args