diff --git a/tests/builtins/test_config b/tests/builtins/test_config
index d282269ed89929da84ca7ef530b8a264f3051d11..e5aae7331927957a07fa55967355b78ed147f1b5 100644
--- a/tests/builtins/test_config
+++ b/tests/builtins/test_config
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
+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 6a1f007bb7c7f9be443b4a1510b2f02e5e4c95b1..98b3a98fc6861091dda33b4cbaca1a2ab5278d4c 100644
--- a/tests/builtins/test_config_apron
+++ b/tests/builtins/test_config_apron
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -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_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 5bf90d048f465b1925efd1fbeb5947b918572b2d..fddf8d55557c30d3d3536b1356b1cfe9e85870ec 100644
--- a/tests/builtins/test_config_bitwise
+++ b/tests/builtins/test_config_bitwise
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-bitwise-domain
+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 b688f61e3ea24b48d7d89c75a861cb6cf6edb9bc..6f71f51c4d9dc983af96581eb9517fa3b7db3be1 100644
--- a/tests/builtins/test_config_equalities
+++ b/tests/builtins/test_config_equalities
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-equality-domain
+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 a0865d46a8ab516cc4d35f68dc40c52504d237ed..3e142f5beb772fe8df5fd28fcfa52c0fa88ba49a 100644
--- a/tests/builtins/test_config_gauges
+++ b/tests/builtins/test_config_gauges
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-gauges-domain
+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 09e7ee9c36386e9da5dd5333b08de8a66afc622d..f5dc3a45b44ea0dd7268899573566c797a79e336 100644
--- a/tests/builtins/test_config_symblocs
+++ b/tests/builtins/test_config_symblocs
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-symbolic-locations-domain
+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/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/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/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; */