[e-acsl] restore -remove-unused-specified-functions

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"

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
 

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 ();

src/plugins/e-acsl/tests/test_config_ci.in

 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