From 40720b2a3041241860a96e1a36ac299fd21c6dba Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 4 Dec 2019 19:38:32 +0100
Subject: [PATCH] [e-acsl] do not monitor compiler built-ins
---
src/plugins/e-acsl/doc/Changelog | 2 ++
.../e-acsl/src/code_generator/global_observer.ml | 14 +++++++++-----
src/plugins/e-acsl/src/code_generator/injector.ml | 4 ++--
src/plugins/e-acsl/src/libraries/misc.ml | 10 +++++++++-
src/plugins/e-acsl/src/libraries/misc.mli | 4 +++-
.../src/project_initializer/dup_functions.ml | 4 ++--
.../e-acsl/src/project_initializer/prepare_ast.ml | 2 +-
7 files changed, 28 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 79d17b198b1..78572f83775 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 a3ab2f4e946..7f3fe8cab77 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 8714ac2538b..c125b9875c9 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 cbc9e16e284..31d7d92833c 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 c1dafb633c9..59ee66f1faf 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 a0e7efedc5e..64fc328a712 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 035f8c083dd..1eee37987db 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
--
GitLab