aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/TargetPrinter.ml11
-rw-r--r--backend/AisAnnot.ml159
-rw-r--r--backend/AisAnnot.mli31
-rw-r--r--backend/PrintAsm.ml24
-rw-r--r--backend/PrintAsmaux.ml12
-rw-r--r--cfrontend/C2C.ml59
-rw-r--r--cparser/Cutil.ml10
-rw-r--r--cparser/Cutil.mli4
-rw-r--r--cparser/Diagnostics.ml8
-rw-r--r--cparser/Diagnostics.mli1
-rw-r--r--cparser/Parse.ml2
-rw-r--r--cparser/Rename.ml2
-rw-r--r--powerpc/TargetPrinter.ml19
-rw-r--r--riscV/TargetPrinter.ml10
-rw-r--r--x86/TargetPrinter.ml10
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
generated by cgit (git 2.34.1) at 2024-06-02 15:59:40 +0000