diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-12-12 13:16:29 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-12-12 13:16:29 +0100 |
| commit | 1057d06826cde79a65dd542c1b4dd72e0c25243d (patch) | |
| tree | 271c50ed19bf21f438acf26abe2afc7582154c23 | |
| parent | f44bf0961c9211cc650a47f73d575658aec4ba77 (diff) | |
| download | compcert-kvx-1057d06826cde79a65dd542c1b4dd72e0c25243d.tar.gz compcert-kvx-1057d06826cde79a65dd542c1b4dd72e0c25243d.zip | |
Deactivate ais_annotations again.
| -rw-r--r-- | cfrontend/C2C.ml | 49 |
1 files changed, 25 insertions, 24 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 173764e3..743ffd3b 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -137,21 +137,22 @@ 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", (TInt(IUInt, []), [TInt(IUInt, [])], false); @@ -865,19 +866,19 @@ 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 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_memcpy_aligned"}}, args) -> make_builtin_memcpy (convertExprList env args) |