From 038715b8916a1d5b1e22513eb8f22a42456efeb3 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 3 Aug 2020 11:59:26 +0200
Subject: [PATCH] [e-acsl] restore -remove-unused-specified-functions
---
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 4 +++-
src/plugins/e-acsl/src/project_initializer/prepare_ast.ml | 4 ----
src/plugins/e-acsl/src/project_initializer/rtl.ml | 3 +--
src/plugins/e-acsl/tests/test_config_ci.in | 2 +-
4 files changed, 5 insertions(+), 8 deletions(-)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 3038810fbf9..aeb097a74df 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -754,7 +754,9 @@ CPPFLAGS="$OPTION_CPPFLAGS"
LDFLAGS="$OPTION_LDFLAGS"
# Extra Frama-C Flags E-ACSL needs
-FRAMAC_FLAGS="$FRAMAC_FLAGS -variadic-no-translation"
+FRAMAC_FLAGS="$FRAMAC_FLAGS \
+ -remove-unused-specified-functions \
+ -variadic-no-translation"
# C, CPP and LD flags for compilation of E-ACSL-generated sources
EACSL_CFLAGS="$OPTION_EXTERNAL_ASSERT"
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 5324a4ffd3b..2c2c73e7cb7 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -482,10 +482,6 @@ class prepare_visitor = object (self)
[ new_decl; g ]
| _ -> assert false)
- | GVarDecl(vi, _loc) | GFunDecl(_, vi, _loc) | GFun({ svar = vi }, _loc)
- when Misc.is_fc_or_compiler_builtin vi ->
- Cil.DoChildren
-
| _ ->
Cil.DoChildren
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index 71e4991ff8b..2a6e9673773 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -34,8 +34,7 @@ let create_rtl_ast prj =
Project.on
prj
(fun () ->
- (* compute the RTL AST in the same settings as the user source code.
- Modifying these settings purposely kills the current AST (if any) *)
+ (* compute the RTL AST in the standard E-ACSL setting *)
if Plugin.is_present "variadic" then
Dynamic.Parameter.Bool.off "-variadic-translation" ();
Kernel.Keep_unused_specified_functions.off ();
diff --git a/src/plugins/e-acsl/tests/test_config_ci.in b/src/plugins/e-acsl/tests/test_config_ci.in
index 0a68607fc71..2530bfd855a 100644
--- a/src/plugins/e-acsl/tests/test_config_ci.in
+++ b/src/plugins/e-acsl/tests/test_config_ci.in
@@ -1,7 +1,7 @@
MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
MACRO: MACHDEP -machdep gcc_x86_64
MACRO: EACSL_PREPARE -e-acsl-prepare -e-acsl-share ./share/e-acsl
-MACRO: GLOBAL @MACHDEP@ -variadic-no-translation -verbose 0
+MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -variadic-no-translation -verbose 0
MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
--
GitLab