From 1057d06826cde79a65dd542c1b4dd72e0c25243d Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 12 Dec 2017 13:16:29 +0100
Subject: Deactivate ais_annotations again.

---
 cfrontend/C2C.ml | 49 +++++++++++++++++++++++++------------------------
 1 file changed, 25 insertions(+), 24 deletions(-)

(limited to 'cfrontend')

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)
-- 
cgit