diff --git a/src/plugins/e-acsl/tests/memory/local_init.c b/src/plugins/e-acsl/tests/memory/local_init.c index 3f088213229d0076f623744b7ba65444efd8ce00..483a08acdeca626a3024b416c9922f1356da660c 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: #"-lib-entry -eva -e-acsl-prepare -e-acsl-share ./share/e-acsl -then -no-lib-entry" + STDOPT: #"@MACHDEP@ @EACSL_PREPARE@ -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 437c1230d3af2162a07800f1fcfd67dea8072677..8cdb54fbcec93c33303e8fdebfa537406b57fb98 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: #"-e-acsl-prepare -e-acsl-share ./share/e-acsl -eva -eva-verbose 0 -then -e-acsl-no-valid" + STDOPT: #"@MACHDEP@ @EACSL_PREPARE@ -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/special/oracle_ci/e-acsl-valid.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle index 8a26335fee12d916f5bdb57b0a8a437933335926..504ec1ce5e1e7ec93e53ba27fd59cb2f6fd01097 100644 --- a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle +++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle @@ -1,5 +1,3 @@ -[eva:alarm] tests/special/e-acsl-valid.c:37: Warning: - function f: precondition \valid(y) got status unknown. [eva:alarm] tests/special/e-acsl-valid.c:37: Warning: function f: precondition \valid(y) got status unknown. [e-acsl] beginning translation. diff --git a/src/plugins/e-acsl/tests/test_config_ci.in b/src/plugins/e-acsl/tests/test_config_ci.in index 7bf6bf598f0dca59d1ae6b98e7ade86a58bcceef..0a68607fc713abce8bf5ac09479dd477ff07e1dd 100644 --- a/src/plugins/e-acsl/tests/test_config_ci.in +++ b/src/plugins/e-acsl/tests/test_config_ci.in @@ -1,5 +1,7 @@ MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@ -MACRO: GLOBAL -machdep gcc_x86_64 -variadic-no-translation -verbose 0 +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: 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