[e-acsl] do not monitor compiler built-ins

src/plugins/e-acsl/doc/Changelog

@@ -19,6 +19,8 @@
 #   configure	configure
 ###############################################################################
 
+-* E-ACSL       [2019/12/04] Fix bug with compiler built-ins.
+
 ############################
 Plugin E-ACSL 20.0 (Calcium)
 ############################

src/plugins/e-acsl/src/code_generator/global_observer.ml

@@ -111,10 +111,12 @@ let mk_init_function () =
   let stmts =
     Varinfo.Hashtbl.fold_sorted
       (fun vi _ stmts ->
-         (* a global is both allocated and initialized *)
-         Constructor.mk_store_stmt vi
-         :: Constructor.mk_initialize ~loc:Location.unknown (Cil.var vi)
-         :: stmts)
+         if Misc.is_fc_or_compiler_builtin vi then stmts
+         else
+           (* a global is both allocated and initialized *)
+           Constructor.mk_store_stmt vi
+           :: Constructor.mk_initialize ~loc:Location.unknown (Cil.var vi)
+           :: stmts)
       tbl
       stmts
   in
@@ -173,7 +175,9 @@ let mk_init_function () =
 
 let mk_delete_stmts stmts =
   Varinfo.Hashtbl.fold_sorted
-    (fun vi _l acc -> Constructor.mk_delete_stmt vi :: acc)
+    (fun vi _l acc ->
+       if Misc.is_fc_or_compiler_builtin vi then acc
+       else Constructor.mk_delete_stmt vi :: acc)
     tbl
     stmts
 

src/plugins/e-acsl/src/code_generator/injector.ml

@@ -593,12 +593,12 @@ let inject_in_global (env, main) = function
 
   (* Cil built-ins and other library globals: nothing to do *)
   | GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
-    when Cil.is_builtin vi ->
+    when Misc.is_fc_or_compiler_builtin vi ->
     env, main
   | g when Misc.is_library_loc (Global.loc g) ->
     env, main
 
-  (* variables and functions declarations *)
+  (* variable declarations *)
   | GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
     (* do not convert extern ghost variables, because they can't be linked,
        see bts #1392 *)

src/plugins/e-acsl/src/libraries/misc.ml

@@ -46,6 +46,14 @@ let register_library_function vi =
 
 let reset () = Datatype.String.Hashtbl.clear library_functions
 
+let is_fc_or_compiler_builtin vi =
+  Cil.is_builtin vi
+  ||
+  (String.length vi.vname >= 10
+   &&
+   let prefix = String.sub vi.vname 0 10 in
+   Datatype.String.equal prefix "__builtin_")
+
 (* ************************************************************************** *)
 (** {2 Builders} *)
 (* ************************************************************************** *)
@@ -215,6 +223,6 @@ let name_of_binop = function
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/libraries/misc.mli

@@ -51,6 +51,8 @@ val is_library_loc: location -> bool
 val register_library_function: varinfo -> unit
 val reset: unit -> unit
 
+val is_fc_or_compiler_builtin: varinfo -> bool
+
 (* ************************************************************************** *)
 (** {2 Other stuff} *)
 (* ************************************************************************** *)
@@ -102,6 +104,6 @@ val finite_min_and_max: Ival.t -> Integer.t * Integer.t
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/project_initializer/dup_functions.ml

@@ -305,7 +305,7 @@ class dup_functions_visitor prj = object (self)
         (* it is duplicable *)
         && self#is_unvariadic_function vi (* it is not a variadic function *)
         && not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
-        && not (Cil.is_builtin vi) (* it is not a Frama-C built-in *)
+        && not (Misc.is_fc_or_compiler_builtin vi) (* it is not a built-in *)
         &&
         (let kf =
            try Globals.Functions.get vi with Not_found -> assert false
@@ -387,7 +387,7 @@ if there are memory-related annotations.@]"
                     but reading some libc code *));
     Cil.JustCopy
   | GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
-      when Cil.is_builtin vi ->
+      when Misc.is_fc_or_compiler_builtin vi ->
     self#next ();
     Cil.JustCopy
   | _ ->

src/plugins/e-acsl/src/project_initializer/prepare_ast.ml

@@ -198,7 +198,7 @@ class prepare_visitor prj = object (self)
     | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
       when self#is_unvariadic_function vi
         && not (Misc.is_library_loc loc)
-        && not (Cil.is_builtin vi)
+        && not (Misc.is_fc_or_compiler_builtin vi)
       ->
       let kf = Extlib.the self#current_kf in
       let s = Annotations.funspec ~populate:false kf in