diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index aeb097a74dfa3380d233083835d2ca765011e62e..1ef4a37607d48dcc3e5848ecd17aa71195526d25 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -557,7 +557,7 @@ do --then) shift; OPTION_THEN=-then - FRAMAC_FLAGS="-e-acsl-prepare $FRAMAC_FLAGS" + FRAMAC_FLAGS="$FRAMAC_FLAGS" ;; # Extra E-ACSL options --e-acsl-extra) diff --git a/src/plugins/e-acsl/tests/memory/local_init.c b/src/plugins/e-acsl/tests/memory/local_init.c index 483a08acdeca626a3024b416c9922f1356da660c..8de0529d5b4ebe3a34852ca95b5cd4d28c4e9816 100644 --- a/src/plugins/e-acsl/tests/memory/local_init.c +++ b/src/plugins/e-acsl/tests/memory/local_init.c @@ -1,7 +1,7 @@ /* run.config_ci COMMENT: test of a local initializer which contains an annotation LOG: gen_@PTEST_NAME@.c - STDOPT: #"@MACHDEP@ @EACSL_PREPARE@ -lib-entry -eva -then -no-lib-entry" + STDOPT: #"@MACHDEP@ -lib-entry -eva -then -no-lib-entry" */ int X = 0; diff --git a/src/plugins/e-acsl/tests/special/e-acsl-valid.c b/src/plugins/e-acsl/tests/special/e-acsl-valid.c index 8cdb54fbcec93c33303e8fdebfa537406b57fb98..f13f228682c83508233deaaafcab494f4b811707 100644 --- a/src/plugins/e-acsl/tests/special/e-acsl-valid.c +++ b/src/plugins/e-acsl/tests/special/e-acsl-valid.c @@ -1,6 +1,6 @@ /* run.config_ci, run.config_dev COMMENT: test option -e-acsl-no-valid - STDOPT: #"@MACHDEP@ @EACSL_PREPARE@ -eva -eva-verbose 0 -then -no-eva -e-acsl-no-valid" + STDOPT: #"@MACHDEP@ -eva -eva-verbose 0 -then -no-eva -e-acsl-no-valid" MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -eva -eva-verbose 0 MACRO: ROOT_EACSL_GCC_OPTS_EXT --then --e-acsl-extra -e-acsl-no-valid */ diff --git a/src/plugins/e-acsl/tests/test_config_ci.in b/src/plugins/e-acsl/tests/test_config_ci.in index 2530bfd855acf218d3e9576d2cbdbfc32752be2a..2c9748e535a049455c62e15f0f0ed3469bc5df95 100644 --- a/src/plugins/e-acsl/tests/test_config_ci.in +++ b/src/plugins/e-acsl/tests/test_config_ci.in @@ -1,6 +1,5 @@ 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@ -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