Skip to content
Snippets Groups Projects
Commit c84d6a32 authored by Basile Desloges's avatar Basile Desloges
Browse files

[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.
parent cca02055
No related branches found
No related tags found
No related merge requests found
/* run.config_ci /* run.config_ci
COMMENT: test of a local initializer which contains an annotation COMMENT: test of a local initializer which contains an annotation
LOG: gen_@PTEST_NAME@.c 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; int X = 0;
......
/* run.config_ci, run.config_dev /* run.config_ci, run.config_dev
COMMENT: test option -e-acsl-no-valid 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_FC_EXTRA_EXT -eva -eva-verbose 0
MACRO: ROOT_EACSL_GCC_OPTS_EXT --then --e-acsl-extra -e-acsl-no-valid MACRO: ROOT_EACSL_GCC_OPTS_EXT --then --e-acsl-extra -e-acsl-no-valid
*/ */
......
[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: [eva:alarm] tests/special/e-acsl-valid.c:37: Warning:
function f: precondition \valid(y) got status unknown. function f: precondition \valid(y) got status unknown.
[e-acsl] beginning translation. [e-acsl] beginning translation.
......
MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@ 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: 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: 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 MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment