diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 79d17b198b14550ca3b0c3b21e044a04a166b24b..78572f83775819071f278b22995fe41e269c545c 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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)
############################
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index a3ab2f4e946f8f16c3940f3fc743fc773b1f25e4..7f3fe8cab77a572492aa980c04870004ae9685da 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 8714ac2538b06636387e9dc57dc7da291d33a233..c125b9875c9f57d4b892d5034c4f6e01bb67ba16 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/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 *)
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index cbc9e16e284ace3ea2b3c1ae17346bc18689a2a2..31d7d92833ce3f995f2f5e7eefaa4f357b9c064a 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/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:
*)
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index c1dafb633c93cd4db90b15f161772c00b4c35f29..59ee66f1faf0f1d20aba65cf85c96855a1a92a25 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/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:
*)
diff --git a/src/plugins/e-acsl/src/project_initializer/dup_functions.ml b/src/plugins/e-acsl/src/project_initializer/dup_functions.ml
index a0e7efedc5e1d53d63988a48f40afb3d559c3344..64fc328a712e224f33e2d6f31fdc0630b825350c 100644
--- a/src/plugins/e-acsl/src/project_initializer/dup_functions.ml
+++ b/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
| _ ->
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 035f8c083dd6ca7277305c4df8200447e7b937de..1eee37987db0534b7caf7f8c7b39660d172e24eb 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/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