Commit e62d4444 authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'bugfix/basile/machdep-with-eva' into 'master'

[eacsl] Fix tests with `-then`

See merge request frama-c/frama-c!2772
parents 0535fad7 c84d6a32
/* 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;
......
/* 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
*/
......
[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.
......
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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment