diff --git a/src/plugins/value/gen_test_config.sh b/src/plugins/value/gen_test_config.sh
index 19d3397f175d76a15f46c86fceb781228ebc3223..b1085f0868634319e144ef3549f4518e100638ca 100755
--- a/src/plugins/value/gen_test_config.sh
+++ b/src/plugins/value/gen_test_config.sh
@@ -6,8 +6,8 @@
# accordingly. The syntax for the root test_config files is as follows
# (2 lines):
#
-# MACRO: VALUECONFIG <options inherited in all tests>
-# OPT: @VALUECONFIG@ <default options, inherited in tests that use STDOPT>
+# MACRO: EVA_CONFIG <options inherited in all tests>
+# OPT: @EVA_CONFIG@ <default options, inherited in tests that use STDOPT>
# All tested domains
declare -a domains=(
diff --git a/tests/builtins/Longinit_sequencer.i b/tests/builtins/Longinit_sequencer.i
index 4d9b50cd565baedf36d4ebb071a2915ff4527216..919f247cf5d6fb7f63b2b76707794dbf2b09428a 100644
--- a/tests/builtins/Longinit_sequencer.i
+++ b/tests/builtins/Longinit_sequencer.i
@@ -1,4 +1,4 @@
/* run.config*
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress -res-file @PTEST_RESULT@
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -res-file @PTEST_RESULT@
*/
diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index d6e1f53181467a2ec7876261086d4a39869f7d19..84322912cb6c9b8a476d38e523f53629faab6d0a 100644
--- a/tests/builtins/big_local_array.i
+++ b/tests/builtins/big_local_array.i
@@ -1,8 +1,8 @@
/* run.config*
-EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs
-OPT: -eva-show-progress -print -journal-disable -eva -report
-OPT: -load-module @PTEST_DIR@/big_local_array_script -then-on prj -print -report
-OPT: -eva-show-progress -print -journal-disable -no-initialized-padding-locals -eva
+ EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs
+ OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report
+ OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/big_local_array_script -then-on prj -print -report
+ OPT: @EVA_OPTIONS@ -print -journal-disable -no-initialized-padding-locals -eva
*/
struct S {
diff --git a/tests/builtins/diff_apron b/tests/builtins/diff_apron
index 6e0afb298cf81be9a26981c03f00a91e38ed717f..7aadf1b8caf55d0626119bd3341e11b5a249e15b 100644
--- a/tests/builtins/diff_apron
+++ b/tests/builtins/diff_apron
@@ -1,12 +1,134 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_apron/Longinit_sequencer.res.oracle
-323c323
+62,65c62,81
+< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
+< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
+< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
+< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
+---
+> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <-
+> main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <-
+> main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <-
+> main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <-
+> main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+153,154c169,216
+< [eva] tests/builtins/long_init.c:93: Reusing old results for call to analyze
+< [eva] tests/builtins/long_init.c:94: Reusing old results for call to analyze
+---
+> [eva] computing for function analyze <- main.
+> Called from tests/builtins/long_init.c:93.
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] Recording results for analyze
+> [eva] Done for function analyze
+> [eva] computing for function analyze <- main.
+> Called from tests/builtins/long_init.c:94.
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] Recording results for analyze
+> [eva] Done for function analyze
+327c389
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_apron/Longinit_sequencer.sav
-562c562
+421,424c483,498
+< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
+< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
+< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
+< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
+---
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init2.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init2.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init2.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init2.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+568c642
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_apron/Longinit_sequencer.sav
+658,661c732,747
+< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
+< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
+< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
+< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
+---
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init3.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init3.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init3.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init3.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_apron/allocated.0.res.oracle
260a261,263
> [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
diff --git a/tests/builtins/diff_bitwise b/tests/builtins/diff_bitwise
index a446ce5ec81906143ed8b4e2f0d3e82eadfd492c..0017418c9fbcf245a0845c9306c4dff7670b008e 100644
--- a/tests/builtins/diff_bitwise
+++ b/tests/builtins/diff_bitwise
@@ -1,9 +1,49 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_bitwise/Longinit_sequencer.res.oracle
-323c323
+153,154c153,188
+< [eva] tests/builtins/long_init.c:93: Reusing old results for call to analyze
+< [eva] tests/builtins/long_init.c:94: Reusing old results for call to analyze
+---
+> [eva] computing for function analyze <- main.
+> Called from tests/builtins/long_init.c:93.
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] Recording results for analyze
+> [eva] Done for function analyze
+> [eva] computing for function analyze <- main.
+> Called from tests/builtins/long_init.c:94.
+> [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
+> [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
+> [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
+> [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
+> [eva] computing for function subanalyze <- analyze <- main.
+> Called from tests/builtins/long_init.c:29.
+> [eva] Recording results for subanalyze
+> [eva] Done for function subanalyze
+> [eva] Recording results for analyze
+> [eva] Done for function analyze
+327c361
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_bitwise/Longinit_sequencer.sav
-562c562
+568c602
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_bitwise/Longinit_sequencer.sav
diff --git a/tests/builtins/diff_equalities b/tests/builtins/diff_equalities
index 534763b2be1b1fcbafd3405c4d4400328f4627b8..bb058d3aba7ea30f147b46ebc76985b65fe71aa9 100644
--- a/tests/builtins/diff_equalities
+++ b/tests/builtins/diff_equalities
@@ -1,9 +1,9 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_equalities/Longinit_sequencer.res.oracle
-323c323
+327c327
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_equalities/Longinit_sequencer.sav
-562c562
+568c568
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_equalities/Longinit_sequencer.sav
diff --git a/tests/builtins/diff_gauges b/tests/builtins/diff_gauges
index f8f6c848e6db0869da3c71efa142db822b36bafe..5a276d3cf19b4a1cf82407e32b8140c371ca444c 100644
--- a/tests/builtins/diff_gauges
+++ b/tests/builtins/diff_gauges
@@ -1,9 +1,9 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_gauges/Longinit_sequencer.res.oracle
-323c323
+327c327
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_gauges/Longinit_sequencer.sav
-562c562
+568c568
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_gauges/Longinit_sequencer.sav
diff --git a/tests/builtins/diff_symblocs b/tests/builtins/diff_symblocs
index fc36c7d36a2c44438169a77e7953a7386a52cbfd..f82ea2c45a6d1e4d65d053350a4b0eadd1ec1c85 100644
--- a/tests/builtins/diff_symblocs
+++ b/tests/builtins/diff_symblocs
@@ -1,9 +1,9 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_symblocs/Longinit_sequencer.res.oracle
-323c323
+327c327
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_symblocs/Longinit_sequencer.sav
-562c562
+568c568
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_symblocs/Longinit_sequencer.sav
diff --git a/tests/builtins/from_result.c b/tests/builtins/from_result.c
index 4c8c5dc55a2729a3ffdb66688668e56ca3ee395b..1076c7ca5bc3f89a20b05d2ab84271e6dd8226ab 100644
--- a/tests/builtins/from_result.c
+++ b/tests/builtins/from_result.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: @VALUECONFIG@ -eva-no-builtins-auto -deps -journal-disable
+ OPT: @EVA_CONFIG@ -eva-no-builtins-auto -deps -journal-disable
*/
#define malloc(n) Frama_C_malloc_fresh(n)
#include "../../share/libc/stdlib.c"
diff --git a/tests/builtins/malloc-deps.i b/tests/builtins/malloc-deps.i
index bd7c49b8400d7153322e5ebb6ca8c88b16f76122..9c514cf7f03c9190fb7da4c1a475532387800a33 100644
--- a/tests/builtins/malloc-deps.i
+++ b/tests/builtins/malloc-deps.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
+ OPT: -eva @EVA_CONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
*/
//@ assigns \result \from \nothing;
void *Frama_C_malloc_fresh(unsigned long n);
diff --git a/tests/builtins/malloc-size-zero.c b/tests/builtins/malloc-size-zero.c
index 4b6d9d25485ae34e6b1ee4f34428569e269764ac..fdb0c68a7895865ceebc92dfed9ccbd6286aeda6 100644
--- a/tests/builtins/malloc-size-zero.c
+++ b/tests/builtins/malloc-size-zero.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -eva-mlevel 3
- OPT: -eva @VALUECONFIG@ -eva-malloc-functions my_calloc
+ OPT: -eva @EVA_CONFIG@ -eva-mlevel 3
+ OPT: -eva @EVA_CONFIG@ -eva-malloc-functions my_calloc
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index fd550da2c4e8e918b56daefc9d2126b8b74126b1..eb00026fa89a438de9352088d7b868c9dadfd809 100644
--- a/tests/builtins/malloc.c
+++ b/tests/builtins/malloc.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -slevel 10 -eva-mlevel 0
+ OPT: -eva @EVA_CONFIG@ -slevel 10 -eva-mlevel 0
*/
void *Frama_C_malloc_by_stack(unsigned long i);
diff --git a/tests/builtins/malloc_bug_tr.c b/tests/builtins/malloc_bug_tr.c
index dd052d1448463d4f7e40640326a9baf333d95f99..98b3d323d6dc902fd725994595d35f248190f46b 100644
--- a/tests/builtins/malloc_bug_tr.c
+++ b/tests/builtins/malloc_bug_tr.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@
+ OPT: -eva @EVA_CONFIG@
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc_memexec.c b/tests/builtins/malloc_memexec.c
index 004e113f6197bbcd78285c831de022ed7d246e7f..463f80de13fe6ee4dd098db987ddb42b46659c44 100644
--- a/tests/builtins/malloc_memexec.c
+++ b/tests/builtins/malloc_memexec.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
+ OPT: -eva @EVA_CONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
*/
//@ assigns \result;
diff --git a/tests/builtins/malloc_multiple.c b/tests/builtins/malloc_multiple.c
index 35e3141ad0c6badb4b13cf31d8dcf6eadf6d5e79..6c807d486a22e8a16f05c7447c7342a1fe0d8f18 100644
--- a/tests/builtins/malloc_multiple.c
+++ b/tests/builtins/malloc_multiple.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -slevel 50 -eva-mlevel 5
+ OPT: -eva @EVA_CONFIG@ -slevel 50 -eva-mlevel 5
*/
#include<stdlib.h>
#define MAX 10
diff --git a/tests/builtins/memcpy_invalid.c b/tests/builtins/memcpy_invalid.c
index 60e26a8463bd46ea2c2c3b9a0e111fedab032d6a..cd0a7b35cf7952616fe681aa8959b5bca7feab6e 100644
--- a/tests/builtins/memcpy_invalid.c
+++ b/tests/builtins/memcpy_invalid.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -journal-disable -calldeps
+ OPT: -eva @EVA_CONFIG@ -journal-disable -calldeps
*/
/*@ assigns \result \from min, max;
diff --git a/tests/builtins/oracle/Longinit_sequencer.res.oracle b/tests/builtins/oracle/Longinit_sequencer.res.oracle
index 6deb10c4aea0a67d5036bafc38745c7f19bd3406..2a0c3fd82a978552927c8aed7b96e5f48b92d07a 100644
--- a/tests/builtins/oracle/Longinit_sequencer.res.oracle
+++ b/tests/builtins/oracle/Longinit_sequencer.res.oracle
@@ -79,6 +79,8 @@
[eva] tests/builtins/long_init.c:77: Call to builtin free
[eva] tests/builtins/long_init.c:77:
function free: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/long_init.c:77:
+ strong free on bases: {__malloc_init_inner_l75}
[eva] Recording results for init_inner
[eva] Done for function init_inner
[eva:locals-escaping] tests/builtins/long_init.c:85: Warning:
@@ -161,6 +163,8 @@
[eva] tests/builtins/long_init.c:103: Call to builtin free
[eva] tests/builtins/long_init.c:103:
function free: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/long_init.c:103:
+ strong free on bases: {__malloc_init_inner_l73}
[eva] tests/builtins/long_init.c:104:
Call to builtin Frama_C_malloc_fresh for function malloc
[eva] tests/builtins/long_init.c:104: allocating variable __malloc_main_l104
@@ -435,6 +439,8 @@ Values at end of function main:
[eva] tests/builtins/long_init2.c:103: Call to builtin free
[eva] tests/builtins/long_init2.c:103:
function free: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/long_init2.c:103:
+ strong free on bases: {__malloc_init_inner_l73}
[eva] tests/builtins/long_init2.c:104:
Call to builtin Frama_C_malloc_fresh for function malloc
[eva] tests/builtins/long_init2.c:104: allocating variable __malloc_main_l104
@@ -670,6 +676,8 @@ Values at end of function main:
[eva] tests/builtins/long_init3.c:103: Call to builtin free
[eva] tests/builtins/long_init3.c:103:
function free: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/long_init3.c:103:
+ strong free on bases: {__malloc_init_inner_l73}
[eva] tests/builtins/long_init3.c:104:
Call to builtin Frama_C_malloc_fresh for function malloc
[eva] tests/builtins/long_init3.c:104: allocating variable __malloc_main_l104
diff --git a/tests/builtins/test_config b/tests/builtins/test_config
index 08ed11b4566bf3ec0f00076bee9a279351f7f06e..e5aae7331927957a07fa55967355b78ed147f1b5 100644
--- a/tests/builtins/test_config
+++ b/tests/builtins/test_config
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_apron b/tests/builtins/test_config_apron
index 376825b23c64d0264068c5a6d1e310c6af6a97a0..98b3a98fc6861091dda33b4cbaca1a2ab5278d4c 100644
--- a/tests/builtins/test_config_apron
+++ b/tests/builtins/test_config_apron
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-apron-oct -eva-msg-key experimental-ok
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-apron-oct -eva-msg-key experimental-ok
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_bitwise b/tests/builtins/test_config_bitwise
index a7dce705feff619ade24257304db07538dbb57bb..fddf8d55557c30d3d3536b1356b1cfe9e85870ec 100644
--- a/tests/builtins/test_config_bitwise
+++ b/tests/builtins/test_config_bitwise
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-bitwise-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-bitwise-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_equalities b/tests/builtins/test_config_equalities
index bdbf2638f30424ef954f1f1d3980ce0080fcda8f..6f71f51c4d9dc983af96581eb9517fa3b7db3be1 100644
--- a/tests/builtins/test_config_equalities
+++ b/tests/builtins/test_config_equalities
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-equality-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-equality-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_gauges b/tests/builtins/test_config_gauges
index 49a71af4206b1ca590f23640858ace79657137e2..3e142f5beb772fe8df5fd28fcfa52c0fa88ba49a 100644
--- a/tests/builtins/test_config_gauges
+++ b/tests/builtins/test_config_gauges
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-gauges-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-gauges-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_symblocs b/tests/builtins/test_config_symblocs
index 1e778cb966369efbec9b7663111bbff65f172626..f5dc3a45b44ea0dd7268899573566c797a79e336 100644
--- a/tests/builtins/test_config_symblocs
+++ b/tests/builtins/test_config_symblocs
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-symbolic-locations-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-symbolic-locations-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/write-const.c b/tests/builtins/write-const.c
index 1dc31cf43b1b253b132f814b145b8b902180c92b..89dfcdd91ae135416df8d7ce0d91a279f41d1235 100644
--- a/tests/builtins/write-const.c
+++ b/tests/builtins/write-const.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -journal-disable -eva-builtins-auto -calldeps
+ OPT: -eva @EVA_CONFIG@ -journal-disable -eva-builtins-auto -calldeps
*/
// This test verifies that writing in a memory location that may be const
diff --git a/tests/constant_propagation/bts117.c b/tests/constant_propagation/bts117.c
index d7cd4b19655b51245d96a82ad57d79545b7d78e4..420cd12e426c82096ca8e4d57efc742b1e5258c8 100644
--- a/tests/constant_propagation/bts117.c
+++ b/tests/constant_propagation/bts117.c
@@ -1,7 +1,7 @@
/* run.config
OPT: -journal-disable -print
-OPT: -journal-disable -semantic-const-folding -eva-show-progress
-OPT: -journal-disable -sparecode-analysis -eva-show-progress
+OPT: -journal-disable -semantic-const-folding @EVA_OPTIONS@
+OPT: -journal-disable -sparecode-analysis @EVA_OPTIONS@
*/
int main1 (void) {
diff --git a/tests/constant_propagation/const_propagate.c b/tests/constant_propagation/const_propagate.c
index 4e9024ceedf1a4f63efb1d15aa1f8c00bcbd7a03..064fee49c0ef0e892a9850a3d8acc80e410265bb 100644
--- a/tests/constant_propagation/const_propagate.c
+++ b/tests/constant_propagation/const_propagate.c
@@ -1,6 +1,6 @@
/* run.config
- OPT: -eva -eva-show-progress -deps -out -input -scf -eva-show-progress -journal-disable
- OPT: -scf -eva-show-progress -cast-from-constant -semantic-const-fold add3 -main init -journal-disable
+ OPT: -eva @EVA_OPTIONS@ -deps -out -input -scf -journal-disable
+ OPT: -scf @EVA_OPTIONS@ -cast-from-constant -semantic-const-fold add3 -main init -journal-disable
*/
int x,y,z;
int TAB[10];
diff --git a/tests/constant_propagation/declaration.c b/tests/constant_propagation/declaration.c
index 69495694b6976ebe6102494fd4bd557e51575776..a9c764d083b25bd9e53713929dc60bf5cc33d995 100644
--- a/tests/constant_propagation/declaration.c
+++ b/tests/constant_propagation/declaration.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -eva -eva-show-progress -then -scf -eva-show-progress -then-on propagated -scf -eva-show-progress
+ OPT: -eva @EVA_OPTIONS@ -then -scf -then-on propagated -scf @EVA_OPTIONS@
*/
void f(int *x, int *y, void (*p)(int *x, int *y)) {
diff --git a/tests/constant_propagation/declaration2.c b/tests/constant_propagation/declaration2.c
index 0c2135f988d0674654f58233887f521e7fe77fc4..f44053abbdf2bfc33b6fca16e20033e8155f84b9 100644
--- a/tests/constant_propagation/declaration2.c
+++ b/tests/constant_propagation/declaration2.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -eva -eva-show-progress -scf -eva-show-progress -journal-disable
+ OPT: -eva @EVA_OPTIONS@ -scf -journal-disable
*/
void f(int *x) { (*x)++; }
diff --git a/tests/constant_propagation/introduction_of_non_explicit_cast.c b/tests/constant_propagation/introduction_of_non_explicit_cast.c
index 9e95b6e88db2c472e56cd47ad852b696c28e2a8b..959842971acaa01ca6b96c2891898086bd098d45 100644
--- a/tests/constant_propagation/introduction_of_non_explicit_cast.c
+++ b/tests/constant_propagation/introduction_of_non_explicit_cast.c
@@ -1,6 +1,6 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva -eva-show-progress -deps -journal-disable
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva @EVA_OPTIONS@ -deps -journal-disable
*/
int x,y,z;
diff --git a/tests/constant_propagation/test_config b/tests/constant_propagation/test_config
index b174b4500a1e5b4372bf921c6966f5355688c4b3..850779adb25d797c03ebc59655d31bec1c50cadf 100644
--- a/tests/constant_propagation/test_config
+++ b/tests/constant_propagation/test_config
@@ -1 +1 @@
-OPT: -journal-disable -scf -eva-show-progress
+OPT: -journal-disable -scf @EVA_OPTIONS@
diff --git a/tests/float/absorb.c b/tests/float/absorb.c
index ca3e781a5f7aa215aeca70d81e08c798a4d5cecf..a71117b1674d5f6ba2b6dc97aeacd836c6f275cd 100644
--- a/tests/float/absorb.c
+++ b/tests/float/absorb.c
@@ -1,7 +1,7 @@
/* run.config
COMMENT: run.config is intentionally not-*
EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err FRAMAC_PLUGIN=tests/.empty @frama-c@ -journal-disable -save @PTEST_DIR@/result/absorb.sav @PTEST_FILE@ > @PTEST_DIR@/result/absorb_sav.res 2> @PTEST_DIR@/result/absorb_sav.err
- EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load @PTEST_DIR@/result/absorb.sav -eva @VALUECONFIG@ -journal-disable -float-hex -save @PTEST_DIR@/result/absorb.sav2 > @PTEST_DIR@/result/absorb_sav2.res 2> @PTEST_DIR@/result/absorb_sav2.err
+ EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load @PTEST_DIR@/result/absorb.sav -eva @EVA_CONFIG@ -journal-disable -float-hex -save @PTEST_DIR@/result/absorb.sav2 > @PTEST_DIR@/result/absorb_sav2.res 2> @PTEST_DIR@/result/absorb_sav2.err
OPT: -load @PTEST_DIR@/result/absorb.sav2 -deps -out -input
*/
/* run.config*
diff --git a/tests/float/alarms.i b/tests/float/alarms.i
index 4ab597abb76b7592135f018689a32dc1d2686927..8d60a075054d3ed035311ea24ecb62b5f24405c9 100644
--- a/tests/float/alarms.i
+++ b/tests/float/alarms.i
@@ -1,7 +1,7 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -warn-special-float non-finite
- OPT: -eva @VALUECONFIG@ -warn-special-float nan
- OPT: -eva @VALUECONFIG@ -warn-special-float none
+ OPT: -eva @EVA_CONFIG@ -warn-special-float non-finite
+ OPT: -eva @EVA_CONFIG@ -warn-special-float nan
+ OPT: -eva @EVA_CONFIG@ -warn-special-float none
*/
union { long long l ; float f ; double d ; } u1, u2;
diff --git a/tests/float/builtins.c b/tests/float/builtins.c
index cd0301afa3e51432ff7ecdfa071d1f8f7c96df56..1b2d53069a31c06abd0b437c3a1b388ed79672e0 100644
--- a/tests/float/builtins.c
+++ b/tests/float/builtins.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -then -main main_log_exp
+ OPT: -eva @EVA_CONFIG@ -then -main main_log_exp
*/
#include <__fc_builtin.h>
diff --git a/tests/float/cond.c b/tests/float/cond.c
index 10ff9866c0400d46f60f48043dbd39e128ab0e40..89cc751c13707df7addc5024e5e5b5aae556091e 100644
--- a/tests/float/cond.c
+++ b/tests/float/cond.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -journal-disable -float-hex
+ OPT: -eva @EVA_CONFIG@ -journal-disable -float-hex
*/
#include "__fc_builtin.h"
diff --git a/tests/float/const.i b/tests/float/const.i
index 24140b0286fc7f72aa5d369cc8836dbacac310a5..9e47e611f885b5ad64dbcd15eaeb52c02cde7d27 100644
--- a/tests/float/const.i
+++ b/tests/float/const.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -float-hex -warn-decimal-float all -journal-disable -then -out -deps
+ OPT: -eva @EVA_CONFIG@ -float-hex -warn-decimal-float all -journal-disable -then -out -deps
*/
typedef double mydouble;
diff --git a/tests/float/extract_bits.i b/tests/float/extract_bits.i
index 1bbd4aa10ec7f42962669a27176be2df8bc27001..2f1c3b541cf97a2988bad93da7b58dca27a567bf 100644
--- a/tests/float/extract_bits.i
+++ b/tests/float/extract_bits.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -warn-decimal-float all
- OPT: -eva @VALUECONFIG@ -slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -warn-decimal-float all
+ OPT: -eva @EVA_CONFIG@ -slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -warn-decimal-float all
+ OPT: -eva @EVA_CONFIG@ -slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -warn-decimal-float all
*/
float f = 3.14;
diff --git a/tests/float/init_float.i b/tests/float/init_float.i
index 9812272d6da6acebefa819ebe849ad279f9d048f..83d69d1336e42e0cdb64c82e99409c770eba553f 100644
--- a/tests/float/init_float.i
+++ b/tests/float/init_float.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -journal-disable -float-normal -lib-entry
+ OPT: -eva @EVA_CONFIG@ -journal-disable -float-normal -lib-entry
*/
typedef struct S { float y; } S;
diff --git a/tests/float/nonlin.c b/tests/float/nonlin.c
index 47d55d67984bbacb51405f8c641d2c34ce5e6b35..fce3e9bc0c74fc2676ab43a99f858d5f474848bd 100644
--- a/tests/float/nonlin.c
+++ b/tests/float/nonlin.c
@@ -1,8 +1,8 @@
/* run.config*
- OPT: -eva-msg-key nonlin -slevel 30 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 0
- OPT: -eva-msg-key nonlin -slevel 30 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
- OPT: -eva-msg-key nonlin -slevel 30 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 0
- OPT: -eva-msg-key nonlin -slevel 30 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
+ OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 0
+ OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
+ OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 0
+ OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
*/
#include "__fc_builtin.h"
diff --git a/tests/float/precise_cos_sin.c b/tests/float/precise_cos_sin.c
index d7f40d0632ff0fb6bcbd7637885260b7dfdf842c..19fde982cfb2f8367bf5c8b2c201a61dec312b8b 100644
--- a/tests/float/precise_cos_sin.c
+++ b/tests/float/precise_cos_sin.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -slevel 1000 -journal-disable -float-normal
+ OPT: -eva @EVA_CONFIG@ -slevel 1000 -journal-disable -float-normal
*/
#include <__fc_builtin.h>
diff --git a/tests/float/round10d.i b/tests/float/round10d.i
index b167a89914ec4c85fe3157c8f4ea75c2c44837bb..a11f0172affbc62e6d6e3c270aa8887463b70d62 100644
--- a/tests/float/round10d.i
+++ b/tests/float/round10d.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -float-normal -journal-disable -no-results
+ OPT: -eva @EVA_CONFIG@ -float-normal -journal-disable -no-results
*/
int main()
diff --git a/tests/float/some.c b/tests/float/some.c
index e8b66bfbd66016d1b7d601951a4156400f417ca7..d7713ce8d71d088a7ba48407e83dfc02d1901648 100644
--- a/tests/float/some.c
+++ b/tests/float/some.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva-show-slevel 10 -slevel 100 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=double -DN=55" -float-normal -journal-disable -no-results
- OPT: -slevel 100 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=float -DN=26" -float-normal -journal-disable -no-results
+ OPT: -eva-show-slevel 10 -slevel 100 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double -DN=55" -float-normal -journal-disable -no-results
+ OPT: -slevel 100 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float -DN=26" -float-normal -journal-disable -no-results
*/
FLOAT t[N] = { 1. } ;
diff --git a/tests/float/special_floats.i b/tests/float/special_floats.i
index ae1b880cdcde14eeca533df5129443f1563eaff7..191afecec7da2c637a90355d92a23dbab8bb23d0 100644
--- a/tests/float/special_floats.i
+++ b/tests/float/special_floats.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -warn-special-float none
+ OPT: -eva @EVA_CONFIG@ -warn-special-float none
*/
/* Tests on special float values NaN and infinites. */
diff --git a/tests/impact/test_config b/tests/impact/test_config
index 867181e4aa33cdc439cb2b044e2c409f9e79f752..c449d18f602ef2fe815b38e0f2cdc3d467e1c815 100644
--- a/tests/impact/test_config
+++ b/tests/impact/test_config
@@ -1 +1 @@
-OPT: -journal-disable -impact-print -eva-show-progress
+OPT: -journal-disable -impact-print @EVA_OPTIONS@
diff --git a/tests/journal/control.i b/tests/journal/control.i
index 8a7acc8e682ff542811632ac5f9436e3a9a0f4f9..a136fc4ec7a9ab6ed04a524260be23695e81cb7d 100644
--- a/tests/journal/control.i
+++ b/tests/journal/control.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: do not compare generated journals since they depend on current time
- EXECNOW: BIN control_journal.ml BIN control_journal_bis.ml (./bin/toplevel.opt -journal-enable -check -eva -deps -out -eva-show-progress -main f -journal-name tests/journal/result/control_journal.ml tests/journal/control.i && cp tests/journal/result/control_journal.ml tests/journal/result/control_journal_bis.ml) > /dev/null 2> /dev/null
+ EXECNOW: BIN control_journal.ml BIN control_journal_bis.ml (./bin/toplevel.opt -journal-enable -check -eva -deps -out @EVA_OPTIONS@ -main f -journal-name tests/journal/result/control_journal.ml tests/journal/control.i && cp tests/journal/result/control_journal.ml tests/journal/result/control_journal_bis.ml) > /dev/null 2> /dev/null
CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
OPT: -load-script tests/journal/result/control_journal -journal-disable
CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index 40d98270dc8eff9237744fe29ebf4c816fa0b825..2fa988b1e5dc0edf41ab46dd4743b4a77b728a36 100644
--- a/tests/libc/coverage.c
+++ b/tests/libc/coverage.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva-no-builtins-auto -eva-show-progress share/libc/string.c -eva -slevel 6 -metrics-eva-cover -then -metrics-libc
+ OPT: -eva-no-builtins-auto @EVA_OPTIONS@ share/libc/string.c -eva -slevel 6 -metrics-eva-cover -then -metrics-libc
*/
#include "string.h"
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 7f27becef31786b70e483b2adeda229886900278..7f19d6c406affaba44102e28bf009c3fd50535c2 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -2,7 +2,7 @@
EXECNOW: make -s @PTEST_DIR@/check_libc_naming_conventions.cmxs
EXECNOW: make -s @PTEST_DIR@/check_const.cmxs
EXECNOW: make -s @PTEST_DIR@/check_parsing_individual_headers.cmxs
- OPT: -load-module @PTEST_DIR@/check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module @PTEST_DIR@/check_const -load-module metrics -eva @VALUECONFIG@ -then -lib-entry -no-print -metrics-no-libc
+ OPT: -load-module @PTEST_DIR@/check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module @PTEST_DIR@/check_const -load-module metrics -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
OPT: -print -print-libc
OPT: -load-module @PTEST_DIR@/check_parsing_individual_headers
CMD: ./tests/libc/check_full_libc.sh
diff --git a/tests/libc/test_config b/tests/libc/test_config
index b4e089126e464d84fb2a71e38521bdf4e07a07a7..cf5c5bb18359425ba47e530ac8c06c936f24d7e8 100644
--- a/tests/libc/test_config
+++ b/tests/libc/test_config
@@ -1 +1 @@
-OPT: -eva -eva-show-progress -cpp-extra-args='-nostdinc -Ishare/libc'
+OPT: -eva @EVA_CONFIG@ -cpp-extra-args='-nostdinc -Ishare/libc'
diff --git a/tests/misc/bts0541.c b/tests/misc/bts0541.c
index 4eb6a3004bab742c81fa24c2bb4d3567b9d01a6b..6bbabaaa30cadda796dfc7d69e53074fb4058368 100644
--- a/tests/misc/bts0541.c
+++ b/tests/misc/bts0541.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -pp-annot -cpp-extra-args="-I./share/libc" -pp-annot -eva -eva-show-progress
+ OPT: -pp-annot -cpp-extra-args="-I./share/libc" -pp-annot -eva @EVA_CONFIG@
*/
#include <stdbool.h>
diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i
index 54f633c7beacbf0a298590ec7bd5efb20003b577..5650e0651c86a321f57387978b130a56e1f889b6 100644
--- a/tests/misc/bts1347.i
+++ b/tests/misc/bts1347.i
@@ -1,6 +1,6 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress -then -report
+ OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then -report
*/
int f(int *x) { return *x; }
int g(int *x) { return *(x++); }
diff --git a/tests/misc/issue109.i b/tests/misc/issue109.i
index 51c709c227b1c61c905901b787e50e87c0825216..e6d7a20671adcc1bc1e8fd39bb40fec6d3986a45 100644
--- a/tests/misc/issue109.i
+++ b/tests/misc/issue109.i
@@ -1,6 +1,6 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva -eva-show-progress -slevel-function main:10 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -eva @EVA_CONFIG@ -slevel-function main:10 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
void main() {
int i, j = 0;
diff --git a/tests/misc/log_twice.i b/tests/misc/log_twice.i
index e5c6f3a5f23f1f5e9fbe1a0f713c81101ead221d..1c1ed1cb63f2918ef0516de494e301c62fd70f04 100644
--- a/tests/misc/log_twice.i
+++ b/tests/misc/log_twice.i
@@ -1,6 +1,6 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva-show-progress
+ OPT: @EVA_CONFIG@ -load-module @PTEST_DIR@/@PTEST_NAME@
*/
int* f() {
diff --git a/tests/misc/widen_hints.c b/tests/misc/widen_hints.c
index 8badf6af2b748ac2011402a6bffbf106304aff26..9791791713a0969b77c7df865881d4d485122d32 100644
--- a/tests/misc/widen_hints.c
+++ b/tests/misc/widen_hints.c
@@ -1,8 +1,8 @@
/* run.config
- OPT: -eva -eva-show-progress -cpp-extra-args=-DSYNTAX_ERRORS -kernel-warn-key=annot-error=active
- OPT: -eva -eva-show-progress -cpp-extra-args=-DNONCONST
- OPT: -eva -eva-show-progress -slevel 1 -eva-msg-key widen-hints
- OPT: -eva -eva-show-progress -cpp-extra-args=-DALLGLOBAL -eva-msg-key widen-hints
+ OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DSYNTAX_ERRORS -kernel-warn-key=annot-error=active
+ OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DNONCONST
+ OPT: -eva @EVA_CONFIG@ -slevel 1 -eva-msg-key widen-hints
+ OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DALLGLOBAL -eva-msg-key widen-hints
*/
#define N 2
diff --git a/tests/pdg/bts1194.c b/tests/pdg/bts1194.c
index 3cebc895ed25e62a66ab7bdad6b0af4149f2b79f..baa829837c3a54216aac8310f110bc0ee53fb35d 100644
--- a/tests/pdg/bts1194.c
+++ b/tests/pdg/bts1194.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-eva -inout -pdg -calldeps -deps -then -slice-return main -then-last -print -eva-show-progress"
+ STDOPT: +"-eva -inout -pdg -calldeps -deps -then -slice-return main -then-last -print @EVA_OPTIONS@"
*/
int Y, X;
diff --git a/tests/pdg/test_config b/tests/pdg/test_config
index 864d6b8a7b681dec8176de949034cf6197aa3b73..d9d741191d10ade715f1080b42b4a421d0d5e4c1 100644
--- a/tests/pdg/test_config
+++ b/tests/pdg/test_config
@@ -1 +1 @@
-OPT: -journal-disable -eva-show-progress -pdg-print -pdg-verbose 2
+OPT: -journal-disable @EVA_OPTIONS@ -pdg-print -pdg-verbose 2
diff --git a/tests/rte/value_rte.c b/tests/rte/value_rte.c
index a1ae69841b33ab5c06307eb0f2bdf5446d61e0ea..0587fca439d1864503ee51cac0cbafb41e217127 100644
--- a/tests/rte/value_rte.c
+++ b/tests/rte/value_rte.c
@@ -1,5 +1,5 @@
/* run.config
-OPT: -rte -then -eva-show-progress -eva -then -report
+OPT: -rte -then -eva @EVA_OPTIONS@ -then -report
*/
#include "stdio.h"
diff --git a/tests/saveload/test_config b/tests/saveload/test_config
index 16c72227f60606ee00121bf18bf95a4d0736fe19..1712a20359b38feaedc7a61eec51ffa3aebc9879 100644
--- a/tests/saveload/test_config
+++ b/tests/saveload/test_config
@@ -1 +1 @@
-OPT: -eva-show-progress
+OPT: @EVA_OPTIONS@
diff --git a/tests/scope/bts383.c b/tests/scope/bts383.c
index dcee5c7978a9d72abfe8fc323c854ac0bfe2026e..db156cbcfc2619ecba73c24ce6c579bdeec6daee 100644
--- a/tests/scope/bts383.c
+++ b/tests/scope/bts383.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -eva -eva-show-progress -print -journal-disable -scope-verbose 1 -remove-redundant-alarms -context-width 3
+ OPT: -eva @EVA_CONFIG@ -print -journal-disable -scope-verbose 1 -remove-redundant-alarms -context-width 3
*/
/*
echo '!Db.Scope.check_asserts();;' \
diff --git a/tests/scope/no-effect.i b/tests/scope/no-effect.i
index 916b4fc6fbecb23e138bef398261fbc73b62dbe0..47f41d8fb6b43f9b3a8da29ecc200377f28d7d1b 100644
--- a/tests/scope/no-effect.i
+++ b/tests/scope/no-effect.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: -eva-show-progress -eva -print -journal-disable -scope-verbose 1 -remove-redundant-alarms
+ OPT: @EVA_CONFIG@ -eva -print -journal-disable -scope-verbose 1 -remove-redundant-alarms
*/
typedef struct {
diff --git a/tests/scope/scope.c b/tests/scope/scope.c
index a0c63884270b4303e27a1d51e1b8ad71a7610196..8cb6670e5eea8871fb05c146036b79b19fcdd450 100644
--- a/tests/scope/scope.c
+++ b/tests/scope/scope.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: -eva -eva-show-progress -main f -journal-disable
- OPT: -eva -eva-show-progress -main f2 -journal-disable
- OPT: -eva -eva-show-progress -main loop -journal-disable
+ OPT: -eva @EVA_CONFIG@ -main f -journal-disable
+ OPT: -eva @EVA_CONFIG@ -main f2 -journal-disable
+ OPT: -eva @EVA_CONFIG@ -main loop -journal-disable
*/
/*
* bin/viewer.byte -main f tests/scope/scope.c -eva
diff --git a/tests/scope/zones.c b/tests/scope/zones.c
index 884e57b2162c1665bbac00b98c150d5e02c6373c..acafbd74299ae375c471c6e8fd9274ea62343f4a 100644
--- a/tests/scope/zones.c
+++ b/tests/scope/zones.c
@@ -1,6 +1,6 @@
/* run.config
# EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva -eva-show-progress -journal-disable
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva @EVA_OPTIONS@ -journal-disable
*/
diff --git a/tests/slicing/adpcm.c b/tests/slicing/adpcm.c
index f6a352643ec4432dc377277177d57c54fee20946..559291e8913aa6ed077a415db585d843f46c7667 100644
--- a/tests/slicing/adpcm.c
+++ b/tests/slicing/adpcm.c
@@ -1,6 +1,6 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- STDOPT: +"-eva-show-progress -load-module ./tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -ulevel -1 -deps -slicing-level 2 -journal-disable"
+ STDOPT: +"-load-module ./tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -ulevel -1 -deps -slicing-level 2 -journal-disable"
*/
#include "tests/test/adpcm.c"
diff --git a/tests/slicing/bts336.i b/tests/slicing/bts336.i
index b1f75ffb65cb5cb9e8ae6bc7aa82b5e223031c9d..ddeee83be06b686bfe260bd8d0ee16cf9d59d907 100644
--- a/tests/slicing/bts336.i
+++ b/tests/slicing/bts336.i
@@ -1,12 +1,12 @@
/* run.config
- STDOPT: +"-slice-return main -calldeps -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
- STDOPT: +"-main main2 -slice-return main2 -calldeps -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
- STDOPT: +"-main main3 -slice-return main3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
- STDOPT: +"-journal-disable -main main3 -inout -calldeps -slice-return main3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -no-inout -eva-show-progress"
- STDOPT: +"-journal-disable -main main -calldeps -slice-return main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
- STDOPT: +"-journal-disable -main main4 -calldeps -slice-return main4 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
- STDOPT: +"-journal-disable -main main4 -calldeps -slice-return main4 -slicing-level 3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
- STDOPT: +"-journal-disable -main main5 -calldeps -slice-return main5 -then-on 'Slicing export' -set-project-as-default -print -eva-show-progress -calldeps -slice-return main5 -then-on 'Slicing export 2' -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
+ STDOPT: +"-slice-return main -calldeps -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-main main2 -slice-return main2 -calldeps -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-main main3 -slice-return main3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-journal-disable -main main3 -inout -calldeps -slice-return main3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -no-inout"
+ STDOPT: +"-journal-disable -main main -calldeps -slice-return main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-journal-disable -main main4 -calldeps -slice-return main4 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-journal-disable -main main4 -calldeps -slice-return main4 -slicing-level 3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-journal-disable -main main5 -calldeps -slice-return main5 -then-on 'Slicing export' -set-project-as-default -print @EVA_OPTIONS@ -calldeps -slice-return main5 -then-on 'Slicing export 2' -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
*/
// something to do to have better results...
int T[10];
diff --git a/tests/slicing/bts709.c b/tests/slicing/bts709.c
index baf67e8b2e5cab4a18dc9b3b4a503cb3961bbb5b..325e6ba28661753469776de28c3d337255b0523f 100644
--- a/tests/slicing/bts709.c
+++ b/tests/slicing/bts709.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-eva-show-progress -slice-pragma func -no-unicode -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-slice-pragma func -no-unicode -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
*/
#include <assert.h>
diff --git a/tests/slicing/combine.i b/tests/slicing/combine.i
index 16d12c1adcd6a2813d481d626b1535c4714bb64f..df980abab596c1ed34198d2c0a314bf7166c5f91 100644
--- a/tests/slicing/combine.i
+++ b/tests/slicing/combine.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -journal-disable
+ OPT: @EVA_OPTIONS@ -deps -journal-disable
*/
//@ assigns \result \from x;
diff --git a/tests/slicing/ex_spec_interproc.i b/tests/slicing/ex_spec_interproc.i
index 962dd869e61cbda26e097423225fba45df9b3713..57bc27bc9ff4f32a1bf28d68be996bca9e4ac8c4 100644
--- a/tests/slicing/ex_spec_interproc.i
+++ b/tests/slicing/ex_spec_interproc.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -journal-disable
+ OPT: @EVA_OPTIONS@ -deps -journal-disable
*/
int X, Y;
diff --git a/tests/slicing/horwitz.i b/tests/slicing/horwitz.i
index 0178857313f549f260b26554f05c18a927bde711..d12de9261ad6bc3aeafd7a22b559eb3ecb9ade0e 100644
--- a/tests/slicing/horwitz.i
+++ b/tests/slicing/horwitz.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -slicing-level 0 -journal-disable
+ OPT: @EVA_OPTIONS@ -deps -slicing-level 0 -journal-disable
*/
/* bin/toplevel.opt -deps -eva @PTEST_DIR@/@PTEST_NAME@.c */
diff --git a/tests/slicing/mark_all_slices.i b/tests/slicing/mark_all_slices.i
index d25812226596c855a7380ef38ddc9520f0f0c405..d3008f37ba96e674dd9947b0e430a3aaf3faea41 100644
--- a/tests/slicing/mark_all_slices.i
+++ b/tests/slicing/mark_all_slices.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -slicing-level 3 -no-slice-callers -journal-disable
+ OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -no-slice-callers -journal-disable
*/
int A, B, C, D;
int A2, B2, C2, D2;
diff --git a/tests/slicing/merge.i b/tests/slicing/merge.i
index bf0509784e30e9adfe5159b4e8cff4be9597d3b9..b255a2c2fe73a442d5b5f2d56918a257aa820c91 100644
--- a/tests/slicing/merge.i
+++ b/tests/slicing/merge.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/libAnim.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -slicing-level 3 -journal-disable
+ OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -journal-disable
*/
int G1, G2, G3;
diff --git a/tests/slicing/min_call.i b/tests/slicing/min_call.i
index f7cc89e6a8dd1b8e1b9b580e0a2bdc2dc0457a75..a06325b8a588960a7b3d3c0978a35b97bf7fd4d8 100644
--- a/tests/slicing/min_call.i
+++ b/tests/slicing/min_call.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -lib-entry -main g -journal-disable -slicing-level 3
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main g -journal-disable -slicing-level 3
*/
/* dummy source file in order to test minimal calls feature
diff --git a/tests/slicing/select_by_annot.i b/tests/slicing/select_by_annot.i
index a0cd4471cf1e72b7b7e5ecfc74212bbc83f1bfb2..b7411c47212a70801cbf4c81efff1831369cccd7 100644
--- a/tests/slicing/select_by_annot.i
+++ b/tests/slicing/select_by_annot.i
@@ -1,22 +1,22 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -lib-entry -main main -journal-disable
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -journal-disable
CMD: bin/toplevel.opt
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma modifS -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma f1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma f2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma f4 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma f5 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma f6 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma f7 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-loop-inv f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-assert f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: -eva-show-progress -check -deps -lib-entry -main main -slice-pragma f9 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma modifS -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f4 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f5 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f6 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f7 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-loop-inv f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f9 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
*/
diff --git a/tests/slicing/select_simple.i b/tests/slicing/select_simple.i
index 9883f3ff5832c4114b5d9af361e3bdc732257829..28face32afaf3a7c8e2dbf76ff7cdbb1ca51221f 100644
--- a/tests/slicing/select_simple.i
+++ b/tests/slicing/select_simple.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -journal-disable
+ OPT: @EVA_OPTIONS@ -deps -journal-disable
*/
/* dummy source file in order to test select_simple.ml */
diff --git a/tests/slicing/simple_intra_slice.i b/tests/slicing/simple_intra_slice.i
index 72d49734dd742677dd7b5e775e88e4b3815ec3d6..b4d995b86b2d258f30cc8ed55cc12dd5b303bfbb 100644
--- a/tests/slicing/simple_intra_slice.i
+++ b/tests/slicing/simple_intra_slice.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -no-slice-callers -journal-disable
+ OPT: @EVA_OPTIONS@ -deps -no-slice-callers -journal-disable
*/
int Unknown;
int G;
diff --git a/tests/slicing/slice_no_body.i b/tests/slicing/slice_no_body.i
index 2c58ae1277dcdd908e0b5a56197d85d042d07856..8e97f4c920a7f4f6972d25a7be69257b90dd1adf 100644
--- a/tests/slicing/slice_no_body.i
+++ b/tests/slicing/slice_no_body.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -lib-entry -main h -journal-disable
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main h -journal-disable
*/
int G;
diff --git a/tests/slicing/switch.i b/tests/slicing/switch.i
index 0b1ca36ce07a809cf0c2cbbaec82b11bd2150ed1..2d7bc906d95ae09e4116b73334ad37a405301b2d 100644
--- a/tests/slicing/switch.i
+++ b/tests/slicing/switch.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva-show-progress -deps -journal-disable
+ OPT: @EVA_OPTIONS@ -deps -journal-disable
*/
int main (char choix) {
int x = 0, y = 0, z = 0;
diff --git a/tests/slicing/test_config b/tests/slicing/test_config
index ab88cd0df154fe33b6c212c048e30a2df40dcc28..94edfab69b08faf9a5480298c9c557bcd43226c0 100644
--- a/tests/slicing/test_config
+++ b/tests/slicing/test_config
@@ -1,2 +1,2 @@
EXECNOW: make -s tests/slicing/libSelect.cmxs tests/slicing/libAnim.cmxs
-OPT: -eva-show-progress
+OPT: @EVA_OPTIONS@
diff --git a/tests/slicing/unitialized.c b/tests/slicing/unitialized.c
index 70693467a8a56b37e90c8261ad7b69d62f467caa..ed41732199c096ccf6de91d770fbc71a187316ec 100644
--- a/tests/slicing/unitialized.c
+++ b/tests/slicing/unitialized.c
@@ -1,8 +1,8 @@
/* run.config
- STDOPT: +"-eva-show-progress -slice-pragma g -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-eva-show-progress -slice-assert g -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-eva-show-progress -slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-eva-show-progress -slice-return g -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-slice-pragma g -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-slice-assert g -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-slice-return g -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
*/
#ifdef __FRAMAC__
//@ assigns \result \from \nothing;
diff --git a/tests/slicing/unravel-point.i b/tests/slicing/unravel-point.i
index 02cad10a907353d3c69fac9d4ec29f40417b80d4..dc07a8049c2ceb736ad00d0ea289b81c8a5393e6 100644
--- a/tests/slicing/unravel-point.i
+++ b/tests/slicing/unravel-point.i
@@ -1,9 +1,9 @@
/* run.config
- STDOPT: +"-calldeps -slice-return send1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
- STDOPT: +"-calldeps -slice-return send2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
- STDOPT: +"-calldeps -slice-return send3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
- STDOPT: +"-calldeps -slice-return send4 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
- STDOPT: +"-calldeps -slice-return send1 -slice-return send4 -journal-disable -then-on 'Slicing export' -eva-show-progress -calldeps -slice-return send1_slice_1 -print -then-on 'Slicing export 2' -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -eva-show-progress"
+ STDOPT: +"-calldeps -slice-return send1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-calldeps -slice-return send2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-calldeps -slice-return send3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-calldeps -slice-return send4 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-calldeps -slice-return send1 -slice-return send4 -journal-disable -then-on 'Slicing export' @EVA_OPTIONS@ -calldeps -slice-return send1_slice_1 -print -then-on 'Slicing export 2' -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
diff --git a/tests/slicing/use_spec.i b/tests/slicing/use_spec.i
index 40af146f8c574963dfb115e4737c4462323298d5..72c572818b14025c278fec1863331efcaa55f49a 100644
--- a/tests/slicing/use_spec.i
+++ b/tests/slicing/use_spec.i
@@ -1,6 +1,6 @@
/* run.config
- STDOPT: +" -eva-use-spec f -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -eva-show-progress"
- STDOPT: +"-main main2 -slicing-level 3 -slice-undef-functions -eva-use-spec h -slice-return main2 -journal-disable -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -eva -eva-use-spec='-@all' -eva-show-progress"
+ STDOPT: +" -eva-use-spec f -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i"
+ STDOPT: +"-main main2 -slicing-level 3 -slice-undef-functions -eva-use-spec h -slice-return main2 -journal-disable -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -eva @EVA_OPTIONS@ -eva-use-spec='-@all'"
diff --git a/tests/slicing/variadic.c b/tests/slicing/variadic.c
index 7dbecd492224e739fb97f55c8a8eb8b43944368e..9de40fa3f8165c58332963c040dfa604669dd68a 100644
--- a/tests/slicing/variadic.c
+++ b/tests/slicing/variadic.c
@@ -1,9 +1,9 @@
/* run.config
- STDOPT: +"-eva-show-progress -slice-return f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -print"
- STDOPT: +"-eva-show-progress -slice-return f3 -no-slice-callers -journal-disable -variadic-no-translation -then-last -print"
- STDOPT: +"-eva-show-progress -slice-return f3 -journal-disable -then-on 'Slicing export' -print"
- STDOPT: +"-eva-show-progress -slice-return main -journal-disable -then-on 'Slicing export' -print"
- STDOPT: +"-eva-show-progress -slice-return main -slicing-level 3 -journal-disable -then-on 'Slicing export' -print"
+ STDOPT: +"-slice-return f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -print"
+ STDOPT: +"-slice-return f3 -no-slice-callers -journal-disable -variadic-no-translation -then-last -print"
+ STDOPT: +"-slice-return f3 -journal-disable -then-on 'Slicing export' -print"
+ STDOPT: +"-slice-return main -journal-disable -then-on 'Slicing export' -print"
+ STDOPT: +"-slice-return main -slicing-level 3 -journal-disable -then-on 'Slicing export' -print"
*/
#include "../pdg/variadic.c"
diff --git a/tests/sparecode/test_config b/tests/sparecode/test_config
index f46bc3e3975c2f0f493d728f84b5fc47c7637689..a9330dd48d062e0b27b9bb948a88af6f4250c17a 100644
--- a/tests/sparecode/test_config
+++ b/tests/sparecode/test_config
@@ -1 +1 @@
-OPT: -journal-disable -eva-show-progress -sparecode-debug 1
+OPT: -journal-disable @EVA_OPTIONS@ -sparecode-debug 1
diff --git a/tests/spec/array_typedef.c b/tests/spec/array_typedef.c
index 428631d42b5e38a7a03c48c8e1e2943d65e75ade..86387dcf4273550cd3a88f637d544008c16bacdb 100644
--- a/tests/spec/array_typedef.c
+++ b/tests/spec/array_typedef.c
@@ -1,5 +1,5 @@
/*run.config
- OPT: -print -eva -eva-show-progress -journal-disable
+ OPT: -print -eva @EVA_CONFIG@ -journal-disable
*/
#define IP_FIELD 4
typedef int ip_address[IP_FIELD];
diff --git a/tests/spec/assigns_result.i b/tests/spec/assigns_result.i
index ed6cce9a19e7e03a9b6c8de56c43c3ad16434d38..f850166909efe129536bc4b54cae90447f6dbaaa 100644
--- a/tests/spec/assigns_result.i
+++ b/tests/spec/assigns_result.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-deps -eva-show-progress"
+ STDOPT: +"-deps @EVA_OPTIONS@"
*/
int X,Y;
diff --git a/tests/spec/assigns_void.c b/tests/spec/assigns_void.c
index dd592b430a547283e8d9f1996095edc1a6809d40..6e70195b864bfe5bb5f5d6f5c48ae74d798d9fbf 100644
--- a/tests/spec/assigns_void.c
+++ b/tests/spec/assigns_void.c
@@ -1,6 +1,6 @@
/* run.config
OPT: -print -journal-disable -kernel-warn-key=annot-error=active
- OPT: -eva -eva-show-progress -main g -print -no-annot -journal-disable
+ OPT: -eva @EVA_CONFIG@ -main g -print -no-annot -journal-disable
*/
//@ assigns *x;
void f(void *x);
diff --git a/tests/spec/behavior_assert.c b/tests/spec/behavior_assert.c
index 6b0939f5160e01bf3dce27c5eeba231cb3e5da0f..2f5d7f9760516f5bb73dea22b220b91f2e07edc3 100644
--- a/tests/spec/behavior_assert.c
+++ b/tests/spec/behavior_assert.c
@@ -1,6 +1,6 @@
/* run.config
-OPT: -eva -eva-show-progress -deps -out -input -journal-disable -lib-entry
-OPT: -eva -eva-show-progress -deps -out -input -journal-disable
+OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable -lib-entry
+OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable
*/
int e;
diff --git a/tests/spec/preprocess.c b/tests/spec/preprocess.c
index db8406068d2487fbd9867ce45e9521c5bfe7894b..f22fa57e73e4e7db835a8ea52069c59e3a6c5033 100644
--- a/tests/spec/preprocess.c
+++ b/tests/spec/preprocess.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -pp-annot -eva -eva-show-progress -journal-disable
+ OPT: -pp-annot -eva @EVA_CONFIG@ -journal-disable
*/
// see bts 1357
diff --git a/tests/spec/shifts.c b/tests/spec/shifts.c
index 349f47cc445c70f7e5584348e413c3ecbe4254fa..a7d934e68da3bb28a16e8b0922eb34cc823694dc 100644
--- a/tests/spec/shifts.c
+++ b/tests/spec/shifts.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -eva -eva-show-progress -deps -journal-disable
+ OPT: -eva @EVA_CONFIG@ -deps -journal-disable
*/
int e;
diff --git a/tests/spec/statement_behavior.c b/tests/spec/statement_behavior.c
index a07de2bcdd4b99025cdd3312a06e4c78d774e51a..e91bc04723652701f7477a479ac8abf29fbacac5 100644
--- a/tests/spec/statement_behavior.c
+++ b/tests/spec/statement_behavior.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -eva -eva-show-progress -inout -journal-disable
+ OPT: -eva @EVA_CONFIG@ -inout -journal-disable
*/
/*@ ensures \result == (int)(5 * x);
*/
diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i
index 0786760a68f8f6abcb244f9485e74fdeac8cbee5..edf44c1c372287804691d41291d1cbd5f120a9b7 100644
--- a/tests/syntax/Refresh_visitor.i
+++ b/tests/syntax/Refresh_visitor.i
@@ -1,6 +1,6 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress
+OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs @EVA_OPTIONS@
*/
struct S { int i; };
diff --git a/tests/syntax/copy_visitor.i b/tests/syntax/copy_visitor.i
index 5d4fe0c44c0deb4b80f47c916ca55e43e9f1015b..2f475d79ae7a5ebeaf572e79e97e4b5f533cc833 100644
--- a/tests/syntax/copy_visitor.i
+++ b/tests/syntax/copy_visitor.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-copy -eva -eva-show-progress"
+ STDOPT: +"-copy -eva @EVA_CONFIG@"
*/
struct S {
int a;
diff --git a/tests/syntax/extern_init.i b/tests/syntax/extern_init.i
index f236a513e9376c46b56a968c5ac4f1e2095dea4f..e6773ed70089a517ab8a9499fbeb5b1b49304902 100644
--- a/tests/syntax/extern_init.i
+++ b/tests/syntax/extern_init.i
@@ -1,6 +1,6 @@
/* run.config
-OPT: @PTEST_DIR@/@PTEST_NAME@_1.i @PTEST_DIR@/@PTEST_NAME@_2.i -eva -eva-show-progress
-OPT: @PTEST_DIR@/@PTEST_NAME@_2.i @PTEST_DIR@/@PTEST_NAME@_1.i -eva -eva-show-progress
+OPT: @PTEST_DIR@/@PTEST_NAME@_1.i @PTEST_DIR@/@PTEST_NAME@_2.i -eva @EVA_CONFIG@
+OPT: @PTEST_DIR@/@PTEST_NAME@_2.i @PTEST_DIR@/@PTEST_NAME@_1.i -eva @EVA_CONFIG@
*/
extern int a[] ;
diff --git a/tests/syntax/unroll_labels.i b/tests/syntax/unroll_labels.i
index 16fd8a5807b47b8aaae954366ad91564e839c41e..4807505a70050da90d949df89003324420c7c7ff 100644
--- a/tests/syntax/unroll_labels.i
+++ b/tests/syntax/unroll_labels.i
@@ -1,6 +1,6 @@
/* run.config
- STDOPT: +"-eva -eva-show-progress"
- STDOPT: +"-eva -eva-show-progress -main main2 -slevel 3"
+ STDOPT: +"-eva @EVA_CONFIG@"
+ STDOPT: +"-eva @EVA_CONFIG@ -main main2 -slevel 3"
*/
enum { SIX = 6 } ;
volatile foo;
diff --git a/tests/syntax/unroll_visit.i b/tests/syntax/unroll_visit.i
index f086d3ab95fe99c1d63559bd48f58b21ba9e8596..38d55c380b64b1be5bc5017806f5f0f462ef59e8 100644
--- a/tests/syntax/unroll_visit.i
+++ b/tests/syntax/unroll_visit.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-eva -eva-show-progress -deps -out -input -deps"
+ STDOPT: +"-eva @EVA_CONFIG@ -deps -out -input -deps"
*/
void main() {
/*@ loop pragma UNROLL 2; */
diff --git a/tests/test_config b/tests/test_config
index 2bc92fd4aeaef3826e3b1bbe196cc94e70e5b7d6..10fa9a74e569e6de5964ff808cd032bcaab8d674 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS -eva-show-progress
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_apron b/tests/test_config_apron
index 322d4a9bc6a2ce918eaa1a51add04bfcba58b4da..ccb5342259ce6871ec6fe0580eafa68a41d227bd 100644
--- a/tests/test_config_apron
+++ b/tests/test_config_apron
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-apron-oct -eva-msg-key experimental-ok
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS -eva-show-progress -eva-apron-oct -eva-msg-key experimental-ok
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise
index 8440d81deff7f93a9ffa247948f1249605339f70..146e7721ea21c31e274e3dc99ca7395e814f06ab 100644
--- a/tests/test_config_bitwise
+++ b/tests/test_config_bitwise
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-bitwise-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS -eva-show-progress -eva-bitwise-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_equalities b/tests/test_config_equalities
index 18f6799ed4b473b5b0af8d2cbfa888c5c7b327a8..1e592c46e5ca534cd7636927a4f6d926eb124b8b 100644
--- a/tests/test_config_equalities
+++ b/tests/test_config_equalities
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-equality-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS -eva-show-progress -eva-equality-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_gauges b/tests/test_config_gauges
index 1840804ec6c6798661e77a1e611104ced98e21f3..7e0fb7cbdac0328ebedf501a2b648a00cf6c6b46 100644
--- a/tests/test_config_gauges
+++ b/tests/test_config_gauges
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-gauges-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS -eva-show-progress -eva-gauges-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index 197dd499d60f0879ac68e95ff5fd1d26c6b7dbfc..77ad2e247406b67f866fc55c5e9bc0c6b554ceea 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -1,2 +1,3 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-symbolic-locations-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS -eva-show-progress -eva-symbolic-locations-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/align_char_array.c b/tests/value/align_char_array.c
index 47c94d0dff2742ca5bc640b82e2f9e392dd4a751..de692f2f709f3533998e31d902afee308ad011df 100644
--- a/tests/value/align_char_array.c
+++ b/tests/value/align_char_array.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
*/
diff --git a/tests/value/array_initializer.i b/tests/value/array_initializer.i
index 37bce1c25946172877b9df83ffa41418f038821e..04029accd9cbbc52b82684a435bb807b5c29d50a 100644
--- a/tests/value/array_initializer.i
+++ b/tests/value/array_initializer.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -then -eva-initialization-padding-globals maybe
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals maybe
*/
int t[5] = { [2] = 3 };
diff --git a/tests/value/array_zero_length.i b/tests/value/array_zero_length.i
index 68f536ad5870272b356d4224bfe88b5edefaa2a1..f84a4ebf84a90dfca79e584bfc02975497a704cf 100644
--- a/tests/value/array_zero_length.i
+++ b/tests/value/array_zero_length.i
@@ -1,7 +1,7 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -journal-disable -machdep gcc_x86_32
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -lib-entry -journal-disable -machdep gcc_x86_32
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -lib-entry -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -journal-disable -machdep gcc_x86_32
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable -machdep gcc_x86_32
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable
*/
char T[];
diff --git a/tests/value/base_addr_offset_block_length.i b/tests/value/base_addr_offset_block_length.i
index 6242687662def92ef6f9d0ca4039c63108700f21..4a20889d500dc60519782ff4c15c287bfb360174 100644
--- a/tests/value/base_addr_offset_block_length.i
+++ b/tests/value/base_addr_offset_block_length.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -context-width 3 -then -slevel 3
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -context-width 3 -then -slevel 3
*/
diff --git a/tests/value/big_lib_entry.i b/tests/value/big_lib_entry.i
index c8f5b717e3d969ee3c8284d57de157f8b0d333d7..88a7fbc821ae225258a104cb7fd8e57aa28b6445 100644
--- a/tests/value/big_lib_entry.i
+++ b/tests/value/big_lib_entry.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -lib-entry -context-width 4 -eva-initialization-padding-globals no
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -context-width 4 -eva-initialization-padding-globals no
*/
typedef struct {
diff --git a/tests/value/bitfield_longlong.c b/tests/value/bitfield_longlong.c
index f2736abcc60d1b5cf3ca87090497bb2a8c9ad58e..c2bdb9d6234e025769ac59c269deac5d6f03ec7e 100644
--- a/tests/value/bitfield_longlong.c
+++ b/tests/value/bitfield_longlong.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -cpp-extra-args="-Dprintf=Frama_C_show_each" -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-Dprintf=Frama_C_show_each" -journal-disable
*/
struct X50 {
long long int z:50;
diff --git a/tests/value/bts1306.i b/tests/value/bts1306.i
index 9510829da639426ef19637cd1cb1a0e0806099ba..f6b51b857843812b7e4d12234621aee910cce851 100644
--- a/tests/value/bts1306.i
+++ b/tests/value/bts1306.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -constfold -slevel 0 -eva @VALUECONFIG@ -print -then -slevel 10 -eva -print
+ OPT: -no-autoload-plugins -load-module from,inout,eva -constfold -slevel 0 -eva @EVA_CONFIG@ -print -then -slevel 10 -eva -print
*/
void g(double x) { double y= x*x; }
diff --git a/tests/value/case_analysis.i b/tests/value/case_analysis.i
index ec27af6dac1b22bd763942951b3099bc8c3bef52..7d9214dd079a84c2c58e219dd718d5a27b99bb24 100644
--- a/tests/value/case_analysis.i
+++ b/tests/value/case_analysis.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -slevel 30 -journal-disable -float-normal
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -slevel 30 -journal-disable -float-normal
*/
diff --git a/tests/value/cond_integer_cast_of_float.i b/tests/value/cond_integer_cast_of_float.i
index 3d7605a20e54fd48b99cd0886bb99435dd785afa..3a6d8768ec945afce02f2c361459b3d97e9903f7 100644
--- a/tests/value/cond_integer_cast_of_float.i
+++ b/tests/value/cond_integer_cast_of_float.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @VALUECONFIG@ -no-results -then -float-hex -main mainbis
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -no-results -then -float-hex -main mainbis
*/
typedef double D;
typedef float F;
diff --git a/tests/value/const_typedef.i b/tests/value/const_typedef.i
index 5bbbe2b4ac61247ec64546e56e18a1d24862cc0e..d9f7f3677ca57b9fe40bdc4bfe5b83857a99bc2b 100644
--- a/tests/value/const_typedef.i
+++ b/tests/value/const_typedef.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -print -then -eva @VALUECONFIG@ -lib-entry -no-print
+ OPT: -no-autoload-plugins -load-module inout,eva -print -then -eva @EVA_CONFIG@ -lib-entry -no-print
*/
typedef int INT[3][3];
diff --git a/tests/value/constarraystructlibentry.i b/tests/value/constarraystructlibentry.i
index 60b87c71f9c332c721ce10dc7b097f59eca92fef..96049bcde852de75c8e5efabe6c11fa5d73aca84 100644
--- a/tests/value/constarraystructlibentry.i
+++ b/tests/value/constarraystructlibentry.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -lib-entry -eva-initialization-padding-globals yes -then -eva-initialization-padding-globals no
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -eva-initialization-padding-globals yes -then -eva-initialization-padding-globals no
*/
const int t[] = { 1, 2, 3, 4, 5 } ;
diff --git a/tests/value/context_free.i b/tests/value/context_free.i
index 67ecd1b2ea552d2ceaf2f35225959450711bd72f..19c6fe292ad444d74ab88ef5c0a76fd4c776d76c 100644
--- a/tests/value/context_free.i
+++ b/tests/value/context_free.i
@@ -1,6 +1,6 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -lib-entry -main f -absolute-valid-range 0x200-0x199 -eva-msg-key initial-state -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -main f -absolute-valid-range 0x200-0x199 -eva-msg-key initial-state -journal-disable
*/
diff --git a/tests/value/dead_inout.i b/tests/value/dead_inout.i
index 27070fc23e5626c93bafc1f382a21cef4afc6b0f..8cf0b0271e64bd950206a33e0f67093c1e6bc6c2 100644
--- a/tests/value/dead_inout.i
+++ b/tests/value/dead_inout.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -out -input -inout -inout -main main_all
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -out -input -inout -inout -main main_all
*/
// This tests a potential imprecision with the computation of input and outputs if one forgets to test that a statement is dead
diff --git a/tests/value/div.i b/tests/value/div.i
index c19d8f8bfe5f40bda66cc1a68ed9b30e023aa6c9..dcea8cf46d46eb257041662c2645467b92d170aa 100644
--- a/tests/value/div.i
+++ b/tests/value/div.i
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-load-module scope -remove-redundant-alarms"
- OPT: -no-autoload-plugins -load-module eva,inout -rte -then -eva @VALUECONFIG@
+ OPT: -no-autoload-plugins -load-module eva,inout -rte -then -eva @EVA_CONFIG@
*/
int X,Y,Z1,Z2,T,U1,U2,V,W1,W2;
int a,b,d1,d2,d0,e;
diff --git a/tests/value/fptr.i b/tests/value/fptr.i
index f9d1014262b879b2ebf54f93c7478f098b4691dd..88daeab0630cbe97a44d8fb52def872d8d5f4bdd 100644
--- a/tests/value/fptr.i
+++ b/tests/value/fptr.i
@@ -1,7 +1,7 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -journal-disable -then -deps -out
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -main main_uninit -journal-disable -then -deps -out
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -journal-disable -then -deps -out
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main main_uninit -journal-disable -then -deps -out
*/
int R=77; volatile int v; int n;
diff --git a/tests/value/from_call.i b/tests/value/from_call.i
index 54942abc2008129dc2246818b5ad9c6212d8a156..c510dd876084aec37a27264ef03de9b99b79a65f 100644
--- a/tests/value/from_call.i
+++ b/tests/value/from_call.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,users,eva -calldeps -eva @VALUECONFIG@ -journal-disable -users -then -input
- OPT: -no-autoload-plugins -load-module from,eva @VALUECONFIG@ -deps -show-indirect-deps -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,users,eva -calldeps -eva @EVA_CONFIG@ -journal-disable -users -then -input
+ OPT: -no-autoload-plugins -load-module from,eva @EVA_CONFIG@ -deps -show-indirect-deps -journal-disable
*/
int a,b,c,d;
int x,y,z,t;
diff --git a/tests/value/ilevel.i b/tests/value/ilevel.i
index 9baf2a45b5aae4d3e1853e904aeda6820f51a583..9cb65bf87964896f8b7a5eb3a95918842bd296e8 100644
--- a/tests/value/ilevel.i
+++ b/tests/value/ilevel.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,slicing,sparecode,eva -eva @VALUECONFIG@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48
+ OPT: -no-autoload-plugins -load-module inout,slicing,sparecode,eva -eva @EVA_CONFIG@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48
*/
// Test in particular that ilevel is by-project, even though it is an ocaml ref
volatile int v;
diff --git a/tests/value/incorrect_reduce_expr.i b/tests/value/incorrect_reduce_expr.i
index d82d4c70d9ccde49d1cf918cd7bdbb5e0b5cd5c0..0c7f22f6219efabde4f3dfd99e6eb8e74a44315c 100644
--- a/tests/value/incorrect_reduce_expr.i
+++ b/tests/value/incorrect_reduce_expr.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -absolute-valid-range 32-36
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -absolute-valid-range 32-36
*/
char t[5];
diff --git a/tests/value/inout.i b/tests/value/inout.i
index 886eb013822120623b782ad42c42b08f7af51c88..2e00e3273ace9c6e10ae5ed5e3e74e4578348b9f 100644
--- a/tests/value/inout.i
+++ b/tests/value/inout.i
@@ -1,10 +1,10 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -deps -main inout_11_0 -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -deps -main inout_11_3 -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -deps -main never_terminate -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -deps -main may_not_terminate -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -deps -main call_may_not_terminate -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main inout_11_0 -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main inout_11_3 -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main never_terminate -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main may_not_terminate -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main call_may_not_terminate -journal-disable
*/
int Xt, Xs, Xs_I, Ys, Ys_I, Z, I;
diff --git a/tests/value/inout_formals.i b/tests/value/inout_formals.i
index 6bbf367f21f3af08a8ffb5d644d926d0be1e87a8..96883b0436b0ba18a4cf72be2e6d664b4aabe98e 100644
--- a/tests/value/inout_formals.i
+++ b/tests/value/inout_formals.i
@@ -1,5 +1,5 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -input-with-formals -inout-with-formals
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -input-with-formals -inout-with-formals
*/
int x, y;
diff --git a/tests/value/inout_proto.i b/tests/value/inout_proto.i
index 2ca51c4b0643dd17e3027ca0fffbe8a3264d53af..977b1591fed06b16f136349a8e77f54120595216 100644
--- a/tests/value/inout_proto.i
+++ b/tests/value/inout_proto.i
@@ -1,5 +1,5 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -input-with-formals -inout-with-formals -main main_main
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -input-with-formals -inout-with-formals -main main_main
*/
typedef unsigned char BYTE;
diff --git a/tests/value/limits.c b/tests/value/limits.c
index 081ea91f82d6060b193d7e6c575c6202ebfe3b85..965d689d1099207749cd4e1caab99964a83a2d44 100644
--- a/tests/value/limits.c
+++ b/tests/value/limits.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -warn-signed-overflow
*/
#include <limits.h>
diff --git a/tests/value/logic_ptr_cast.i b/tests/value/logic_ptr_cast.i
index 1d85185f09c75c053457f590b9698a167880738d..6f4c7af2f12976ac4cab2c017bad0db2d826d135 100644
--- a/tests/value/logic_ptr_cast.i
+++ b/tests/value/logic_ptr_cast.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @VALUECONFIG@ -print -journal-disable -no-results
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -print -journal-disable -no-results
*/
int *p;
int t[90];
diff --git a/tests/value/loop_test.i b/tests/value/loop_test.i
index e46589842210d8a573d65205d25fda33eeed05d0..6b1e166139c0aad1abf2f61f4b99233d4639dba5 100644
--- a/tests/value/loop_test.i
+++ b/tests/value/loop_test.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -main test_onzes -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -main test_cent_onzes -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main test_onzes -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main test_cent_onzes -journal-disable
*/
diff --git a/tests/value/loop_wvar.i b/tests/value/loop_wvar.i
index 2d635fae34d26333ef5f8193261b68c6135e0fdd..341e446a0ad758d60a6c278b8609dc472a3ccf8b 100644
--- a/tests/value/loop_wvar.i
+++ b/tests/value/loop_wvar.i
@@ -1,8 +1,8 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -no-annot -eva @VALUECONFIG@ -then -kernel-warn-key=annot-error=active -annot -eva -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout,eva -kernel-warn-key=annot-error=active -eva @VALUECONFIG@ -main main3 -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @VALUECONFIG@ -main main_err1 -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @VALUECONFIG@ -main main_err2 -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -no-annot -eva @EVA_CONFIG@ -then -kernel-warn-key=annot-error=active -annot -eva -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main3 -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main_err1 -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main_err2 -journal-disable
*/
diff --git a/tests/value/loopinv.c b/tests/value/loopinv.c
index 9da813469496b986d7e6d4e5a1134e73011c9f4e..fbb89b089a48133c41a3cfa20648cb9a5b2c633d 100644
--- a/tests/value/loopinv.c
+++ b/tests/value/loopinv.c
@@ -1,5 +1,5 @@
/* run.config*
-OPT: @VALUECONFIG@ -no-autoload-plugins -load-module from,inout,eva,report -slevel-function main2:20 -pp-annot -eva -then -report
+OPT: @EVA_CONFIG@ -no-autoload-plugins -load-module from,inout,eva,report -slevel-function main2:20 -pp-annot -eva -then -report
*/
/*@ requires valid: \valid(&t[0..s-1]);
diff --git a/tests/value/machdep.c b/tests/value/machdep.c
index f2164ce80119b7ca8c4a2872eed611926ea4faa5..b901879416538caefa4fafda266ad349c17d7790 100644
--- a/tests/value/machdep.c
+++ b/tests/value/machdep.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -cpp-extra-args="-DPTEST" -journal-disable -then -machdep x86_64 -then -machdep x86_16
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable -then -machdep x86_64 -then -machdep x86_16
*/
#ifndef PTEST
diff --git a/tests/value/nested_struct_init.i b/tests/value/nested_struct_init.i
index 88d885ee6c8384db3ef2822c7e90cc2d59de17e2..f73a3e08021154c466c6ed2c8201e05a41043ace 100644
--- a/tests/value/nested_struct_init.i
+++ b/tests/value/nested_struct_init.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals maybe -then -lib-entry -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals yes
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals maybe -then -lib-entry -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals yes
*/
typedef signed char int8_t;
diff --git a/tests/value/origin.i b/tests/value/origin.i
index 4be9a4a8f122b25568557980c4387a7ff6b3b21a..e00c59f3ba65d431d9c5512683e561f55d1253a6 100644
--- a/tests/value/origin.i
+++ b/tests/value/origin.i
@@ -1,7 +1,7 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module from,inout,eva @VALUECONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-main -main main -journal-disable -then -out -deps
- OPT: -no-autoload-plugins -load-module from,inout,eva @VALUECONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-origin -main origin -journal-disable -then -out -deps
+ OPT: -no-autoload-plugins -load-module from,inout,eva @EVA_CONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-main -main main -journal-disable -then -out -deps
+ OPT: -no-autoload-plugins -load-module from,inout,eva @EVA_CONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-origin -main origin -journal-disable -then -out -deps
*/
char f(void);
diff --git a/tests/value/postcond_leaf.c b/tests/value/postcond_leaf.c
index b7171d4133a9a6be19c5030b615d8dfacaba0600..37b99f53706ca6690608d4df5d780720fb0afa04 100644
--- a/tests/value/postcond_leaf.c
+++ b/tests/value/postcond_leaf.c
@@ -1,5 +1,5 @@
/* run.config*
-OPT: -no-autoload-plugins @VALUECONFIG@ -load-module eva,inout,report -eva-no-show-progress -eva -eva-use-spec g1,g2,g3 -then -report
+OPT: -no-autoload-plugins @EVA_CONFIG@ -load-module eva,inout,report -eva-no-show-progress -eva -eva-use-spec g1,g2,g3 -then -report
*/
/* Test what is printed when Value evaluates a post-condition:
diff --git a/tests/value/precond.c b/tests/value/precond.c
index 49b21d44e0af2c74f8b6561ba9145ca40d1a111b..a8c73729935defb33716cd1688cef3fb929786fa 100644
--- a/tests/value/precond.c
+++ b/tests/value/precond.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva,report -lib-entry -eva @VALUECONFIG@ -then -report -report-print-properties -then -report-no-specialized
+ OPT: -no-autoload-plugins -load-module from,inout,eva,report -lib-entry -eva @EVA_CONFIG@ -then -report -report-print-properties -then -report-no-specialized
*/
diff --git a/tests/value/precond2.c b/tests/value/precond2.c
index 9008ebd722097da73c7115cc4c3da66ed34d7fb8..be7006c890e03461fa2cc4e79f8cf0d8096d4125 100644
--- a/tests/value/precond2.c
+++ b/tests/value/precond2.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -rte -then -eva @VALUECONFIG@ -then -report -report-print-properties
- OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -eva @VALUECONFIG@ -then -rte -then -report -report-print-properties
+ OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -rte -then -eva @EVA_CONFIG@ -then -report -report-print-properties
+ OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -eva @EVA_CONFIG@ -then -rte -then -report -report-print-properties
*/
// Fuse with precond.c when bts #1208 is solved
diff --git a/tests/value/protomain.i b/tests/value/protomain.i
index 7e8a769384acc1771b082da46945e5b09fffcd2d..ff7e47cb0b4932e85d8ffb3a341b0e4f19e3c604 100644
--- a/tests/value/protomain.i
+++ b/tests/value/protomain.i
@@ -1,4 +1,4 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@
*/
int main(int c, char **);
diff --git a/tests/value/recol.c b/tests/value/recol.c
index a19aaef50165bed715cb30007652c3f057388f80..5d0d3e258cafc1c7999e035c68337ba922a2b1db 100644
--- a/tests/value/recol.c
+++ b/tests/value/recol.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@ -slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -no-warn-signed-overflow
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@ -slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -machdep ppc_32 -no-warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -no-warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -machdep ppc_32 -no-warn-signed-overflow
*/
#ifndef PTEST
diff --git a/tests/value/recursion.i b/tests/value/recursion.i
index a7943ae37f25a02401cc13ed8c93e216c8d37842..2b916a17354f17b3e39f216477a7343128c08a36 100644
--- a/tests/value/recursion.i
+++ b/tests/value/recursion.i
@@ -1,6 +1,6 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @VALUECONFIG@ -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @VALUECONFIG@ -eva-ignore-recursive-calls -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_CONFIG@ -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_CONFIG@ -eva-ignore-recursive-calls -journal-disable
*/
int G;
diff --git a/tests/value/recursion2.i b/tests/value/recursion2.i
index 7b2a209eda2cba2aa4517a3a851906013a2e7a8d..ec3ea022c9c7e35712cf0f8b466c78c91b7ceace 100644
--- a/tests/value/recursion2.i
+++ b/tests/value/recursion2.i
@@ -1,5 +1,5 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -journal-disable -then -input -out -inout
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -journal-disable -then -input -out -inout
*/
int x, y;
diff --git a/tests/value/redundant_alarms.c b/tests/value/redundant_alarms.c
index 662a3f956db495179243bae16f33f6209f9e84b0..cd26fec1a2c7ab4b10c2b944536d16f4ceff23ee 100644
--- a/tests/value/redundant_alarms.c
+++ b/tests/value/redundant_alarms.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,scope,slicing,sparecode @VALUECONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
+ OPT: -no-autoload-plugins -load-module inout,scope,slicing,sparecode @EVA_CONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
**/
volatile int v;
diff --git a/tests/value/replace_by_show_each.c b/tests/value/replace_by_show_each.c
index a100f63626e5ff157442876b01adf7d1aa3f78a1..51592b67f44fd1c183ee2478a67dc16468c4ed9f 100644
--- a/tests/value/replace_by_show_each.c
+++ b/tests/value/replace_by_show_each.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -inout -calldeps
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -inout -calldeps
*/
#define show_each_1 Frama_C_show_each_1
diff --git a/tests/value/sign_of_bitfiled_int.c b/tests/value/sign_of_bitfiled_int.c
index efe30e77e34edefd231fa99d35ab8be77de097d4..b69aa28c06baafceb1534387dc5b661cbbb20ab1 100644
--- a/tests/value/sign_of_bitfiled_int.c
+++ b/tests/value/sign_of_bitfiled_int.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -machdep ppc_32 -eva @VALUECONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -machdep ppc_32 -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
*/
diff --git a/tests/value/simplify_cfg.i b/tests/value/simplify_cfg.i
index 7b0b780c2043eb2ad142d226220985bf961bb137..5c1b0f1d7193e23bfa1bcbc04740b3aacbd5b681 100644
--- a/tests/value/simplify_cfg.i
+++ b/tests/value/simplify_cfg.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -keep-switch -eva @VALUECONFIG@ -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -eva @VALUECONFIG@ -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -keep-switch -eva @EVA_CONFIG@ -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -eva @EVA_CONFIG@ -journal-disable
*/
int main(int x, int y) {
diff --git a/tests/value/ulongvslonglong.i b/tests/value/ulongvslonglong.i
index 54c7fe76c339eabafd4c4b9e6a9f5ade959cdaa2..c945f20f8813505c233ddf76b4df42533726d3bc 100644
--- a/tests/value/ulongvslonglong.i
+++ b/tests/value/ulongvslonglong.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@ -journal-disable -machdep x86_64
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@ -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -journal-disable -machdep x86_64
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -journal-disable
*/
int x;
diff --git a/tests/value/uninit_callstack.i b/tests/value/uninit_callstack.i
index 86a4a5e5e833ea581e74cea8a9f9fb3461c35500..3c1d29d57655fbf18f9134cfc186dd1b45ace78a 100644
--- a/tests/value/uninit_callstack.i
+++ b/tests/value/uninit_callstack.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @VALUECONFIG@ -eva-no-show-progress -eva-print-callstacks -journal-disable -no-results
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -eva-no-show-progress -eva-print-callstacks -journal-disable -no-results
*/
int *p, x;
diff --git a/tests/value/unknown_sizeof.i b/tests/value/unknown_sizeof.i
index 0d06b705a96e26caf96d25728508b9c69e1689fd..f3a1c3c0c65e3ed31968b58d4531746eba71b228 100644
--- a/tests/value/unknown_sizeof.i
+++ b/tests/value/unknown_sizeof.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @VALUECONFIG@ -main main1
- OPT: -no-autoload-plugins -load-module eva -eva @VALUECONFIG@ -main main2
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -main main1
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -main main2
*/
struct s;
diff --git a/tests/value/use_spec.i b/tests/value/use_spec.i
index a98064c85ed784f7ece55286f0d872ab7383b091..b22673b3052ae0dc65f6d85e38de74b386760165 100644
--- a/tests/value/use_spec.i
+++ b/tests/value/use_spec.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @VALUECONFIG@ -inout -calldeps
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @VALUECONFIG@ -inout -calldeps -show-indirect-deps
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps -show-indirect-deps
*/
diff --git a/tests/value/volatile2.i b/tests/value/volatile2.i
index 4a2231374ad7d6cc069910c8ca30067a88b57490..f1088a88553a2248945e46d4bbb132348729c74f 100644
--- a/tests/value/volatile2.i
+++ b/tests/value/volatile2.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -print -eva @VALUECONFIG@ -machdep x86_16
+ OPT: -no-autoload-plugins -load-module from,inout,eva -print -eva @EVA_CONFIG@ -machdep x86_16
*/
diff --git a/tests/value/widen_overflow.i b/tests/value/widen_overflow.i
index 36960e75ecf5e764feac0ea8640e550fac081d7c..9bf6480e8085454da2b1e8bacec7f77ba184285a 100644
--- a/tests/value/widen_overflow.i
+++ b/tests/value/widen_overflow.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@
*/
int main() {