From c84d6a326a805804d83696ad85e3d319e57446df Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 27 Jul 2020 16:23:11 +0200
Subject: [PATCH] [eacsl] Fix tests with `-then`
The option `-machdep` should be called with `-e-acsl-prepare` before the
`-then`, otherwise when `-machdep` is finally used then the project is cleared
and all previous analysis are lost.
---
src/plugins/e-acsl/tests/memory/local_init.c | 2 +-
src/plugins/e-acsl/tests/special/e-acsl-valid.c | 2 +-
.../e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle | 2 --
src/plugins/e-acsl/tests/test_config_ci.in | 4 +++-
4 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/tests/memory/local_init.c b/src/plugins/e-acsl/tests/memory/local_init.c
index 3f088213229..483a08acdec 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 437c1230d3a..8cdb54fbcec 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 8a26335fee1..504ec1ce5e1 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 7bf6bf598f0..0a68607fc71 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
--
GitLab