From 8e6f6df03909e98050dd53cd285adc9740172f90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 4 Apr 2019 11:11:15 +0200
Subject: [PATCH] [tests] Uses the macro EVA_OPTIONS instead of option
-eva-show-progress.
---
tests/builtins/test_config | 2 +-
tests/builtins/test_config_apron | 2 +-
tests/builtins/test_config_bitwise | 2 +-
tests/builtins/test_config_equalities | 2 +-
tests/builtins/test_config_gauges | 2 +-
tests/builtins/test_config_symblocs | 2 +-
tests/constant_propagation/bts117.c | 4 +--
tests/constant_propagation/const_propagate.c | 4 +--
tests/constant_propagation/declaration.c | 2 +-
tests/constant_propagation/declaration2.c | 2 +-
.../introduction_of_non_explicit_cast.c | 2 +-
tests/constant_propagation/test_config | 2 +-
tests/impact/test_config | 2 +-
tests/journal/control.i | 2 +-
tests/libc/coverage.c | 2 +-
tests/libc/test_config | 2 +-
tests/misc/bts0541.c | 2 +-
tests/misc/bts1347.i | 2 +-
tests/misc/issue109.i | 2 +-
tests/misc/log_twice.i | 2 +-
tests/misc/widen_hints.c | 8 ++---
tests/pdg/bts1194.c | 2 +-
tests/pdg/test_config | 2 +-
tests/rte/value_rte.c | 2 +-
tests/saveload/test_config | 2 +-
tests/scope/bts383.c | 2 +-
tests/scope/no-effect.i | 2 +-
tests/scope/scope.c | 6 ++--
tests/scope/zones.c | 2 +-
tests/slicing/adpcm.c | 2 +-
tests/slicing/bts336.i | 16 +++++-----
tests/slicing/bts709.c | 2 +-
tests/slicing/combine.i | 2 +-
tests/slicing/ex_spec_interproc.i | 2 +-
tests/slicing/horwitz.i | 2 +-
tests/slicing/mark_all_slices.i | 2 +-
tests/slicing/merge.i | 2 +-
tests/slicing/min_call.i | 2 +-
tests/slicing/select_by_annot.i | 30 +++++++++----------
tests/slicing/select_simple.i | 2 +-
tests/slicing/simple_intra_slice.i | 2 +-
tests/slicing/slice_no_body.i | 2 +-
tests/slicing/switch.i | 2 +-
tests/slicing/test_config | 2 +-
tests/slicing/unitialized.c | 8 ++---
tests/slicing/unravel-point.i | 10 +++----
tests/slicing/use_spec.i | 4 +--
tests/slicing/variadic.c | 10 +++----
tests/sparecode/test_config | 2 +-
tests/spec/array_typedef.c | 2 +-
tests/spec/assigns_result.i | 2 +-
tests/spec/assigns_void.c | 2 +-
tests/spec/behavior_assert.c | 4 +--
tests/spec/preprocess.c | 2 +-
tests/spec/shifts.c | 2 +-
tests/spec/statement_behavior.c | 2 +-
tests/syntax/Refresh_visitor.i | 2 +-
tests/syntax/copy_visitor.i | 2 +-
tests/syntax/extern_init.i | 4 +--
tests/syntax/unroll_labels.i | 4 +--
tests/syntax/unroll_visit.i | 2 +-
61 files changed, 104 insertions(+), 104 deletions(-)
diff --git a/tests/builtins/test_config b/tests/builtins/test_config
index d282269ed89..e5aae733192 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 6a1f007bb7c..98b3a98fc68 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 5bf90d048f4..fddf8d55557 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 b688f61e3ea..6f71f51c4d9 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 a0865d46a8a..3e142f5beb7 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 09e7ee9c363..f5dc3a45b44 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 d7cd4b19655..420cd12e426 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 4e9024ceedf..064fee49c0e 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 69495694b69..a9c764d083b 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 0c2135f988d..f44053abbdf 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 9e95b6e88db..959842971ac 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 b174b4500a1..850779adb25 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 867181e4aa3..c449d18f602 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 8a7acc8e682..a136fc4ec7a 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 40d98270dc8..2fa988b1e5d 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 b4e089126e4..cf5c5bb1835 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 4eb6a3004ba..6bbabaaa30c 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 54f633c7bea..5650e0651c8 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 51c709c227b..e6d7a20671a 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 e5c6f3a5f23..1c1ed1cb63f 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 8badf6af2b7..9791791713a 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 3cebc895ed2..baa829837c3 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 864d6b8a7b6..d9d741191d1 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 a1ae69841b3..0587fca439d 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 16c72227f60..1712a20359b 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 dcee5c7978a..db156cbcfc2 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 916b4fc6fbe..47f41d8fb6b 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 a0c63884270..8cb6670e5ee 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 884e57b2162..acafbd74299 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 f6a352643ec..559291e8913 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 b1f75ffb65c..ddeee83be06 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 baf67e8b2e5..325e6ba2866 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 16d12c1adcd..df980abab59 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 962dd869e61..57bc27bc9ff 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 0178857313f..d12de9261ad 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 d2581222659..d3008f37ba9 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 bf0509784e3..b255a2c2fe7 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 f7cc89e6a8d..a06325b8a58 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 a0cd4471cf1..b7411c47212 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 9883f3ff583..28face32afa 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 72d49734dd7..b4d995b86b2 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 2c58ae1277d..8e97f4c920a 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 0b1ca36ce07..2d7bc906d95 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 ab88cd0df15..94edfab69b0 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 70693467a8a..ed41732199c 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 02cad10a907..dc07a8049c2 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 40af146f8c5..72c572818b1 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 7dbecd49222..9de40fa3f81 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 f46bc3e3975..a9330dd48d0 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 428631d42b5..86387dcf427 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 ed6cce9a19e..f850166909e 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 dd592b430a5..6e70195b864 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 6b0939f5160..2f5d7f97605 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 db8406068d2..f22fa57e73e 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 349f47cc445..a7d934e68da 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 a07de2bcdd4..e91bc047236 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 0786760a68f..edf44c1c372 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 5d4fe0c44c0..2f475d79ae7 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 f236a513e93..e6773ed7008 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 16fd8a5807b..4807505a700 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 f086d3ab95f..38d55c380b6 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; */
--
GitLab