From ba25aa730abf85964b33eb55c87d1ba6d4c4602f Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 9 Oct 2020 15:58:58 +0200
Subject: [PATCH] [eacsl] Don't process Variadic generated functions
---
src/plugins/e-acsl/src/code_generator/injector.ml | 3 +++
src/plugins/e-acsl/src/libraries/misc.ml | 3 +++
src/plugins/e-acsl/src/libraries/misc.mli | 4 ++++
src/plugins/e-acsl/src/project_initializer/prepare_ast.ml | 2 ++
4 files changed, 12 insertions(+)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 75ec65a7b49..b3d6c65a3d6 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -639,6 +639,9 @@ let inject_in_global (env, main) = function
env, main
| g when Rtl.Symbols.mem_global g ->
env, main
+ (* generated function declaration: nothing to do *)
+ | GFunDecl(_, vi, _) when Misc.is_fc_stdlib_generated vi ->
+ env, main
(* variable declarations *)
| GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 2c123e74461..7aafe514878 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -36,6 +36,9 @@ let is_fc_or_compiler_builtin vi =
let prefix = String.sub vi.vname 0 prefix_length in
Datatype.String.equal prefix "__builtin_")
+let is_fc_stdlib_generated vi =
+ Cil.hasAttribute "fc_stdlib_generated" vi.vattr
+
(* ************************************************************************** *)
(** {2 Handling \result} *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 090b2377531..f5a2c283597 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -40,6 +40,10 @@ val result_vi: kernel_function -> varinfo
val is_fc_or_compiler_builtin: varinfo -> bool
+val is_fc_stdlib_generated: varinfo -> bool
+(** Returns true if the [varinfo] is a generated stdlib function. (For instance
+ generated function by the Variadic plug-in. *)
+
val term_addr_of: loc:location -> term_lval -> typ -> term
val cty: logic_type -> typ
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 2f167b55c03..fd41f2f344d 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -392,6 +392,8 @@ let must_duplicate kf vi =
not (is_variadic_function vi)
&& (* it is not a built-in *)
not (Misc.is_fc_or_compiler_builtin vi)
+ && (* it is not a generated function *)
+ not (Misc.is_fc_stdlib_generated vi)
&&
((* either explicitely listed as to be not instrumented *)
not (Functions.instrument kf)
--
GitLab