diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index 0b931e1f1fe9931cbf0106a9d8f20d62e8f83c22..ce4500f78d0b4c0a6747ae45e1762a34ad5e0eae 100644
--- a/tests/builtins/big_local_array.i
+++ b/tests/builtins/big_local_array.i
@@ -1,5 +1,5 @@
/* run.config*
- PLUGIN: report @EVA_PLUGINS@
+ PLUGIN: report @EVA_CONFIG@
CMXS: big_local_array_script
OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report
OPT: @EVA_OPTIONS@ -load-module %{dep:big_local_array_script.cmxs} -then-on prj -print -report
diff --git a/tests/builtins/from_result.c b/tests/builtins/from_result.c
index e38ba72eb1cb450f66f32242da7b55cf7921ecac..29020e5dbbe0eaafd88a4f3226232abcb79c4f1c 100644
--- a/tests/builtins/from_result.c
+++ b/tests/builtins/from_result.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: @EVA_CONFIG@ -eva-alloc-builtin fresh -deps -journal-disable
+ OPT: @EVA_OPTIONS@ -eva-alloc-builtin fresh -deps -journal-disable
*/
#include "stdlib.c"
diff --git a/tests/builtins/malloc-deps.c b/tests/builtins/malloc-deps.c
index 1bb43e5021c1eb4b3d88ff639219613a9f099871..29f258d52bb00ac6cfe776db7fe0d4ed4a27b9c9 100644
--- a/tests/builtins/malloc-deps.c
+++ b/tests/builtins/malloc-deps.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -deps -calldeps -inout -eva-slevel 5 -eva-msg-key malloc
+ OPT: -eva @EVA_OPTIONS@ -deps -calldeps -inout -eva-slevel 5 -eva-msg-key malloc
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc-size-zero.c b/tests/builtins/malloc-size-zero.c
index 0ff4c5e749f9ed70eb450993db8dcad2226ca561..21cb95cfe5ce572faf9ddabdf5f2034d2582a329 100644
--- a/tests/builtins/malloc-size-zero.c
+++ b/tests/builtins/malloc-size-zero.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -eva-mlevel 3
- OPT: -eva @EVA_CONFIG@ -eva-alloc-functions my_calloc
+ OPT: -eva @EVA_OPTIONS@ -eva-mlevel 3
+ OPT: -eva @EVA_OPTIONS@ -eva-alloc-functions my_calloc
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index 989d36b908624a16151ca3120929f4bce1961862..ad4bffd113a75afb380a9da4bb3f6337ce7d29a8 100644
--- a/tests/builtins/malloc.c
+++ b/tests/builtins/malloc.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -eva-slevel 10 -eva-mlevel 0 -eva-alloc-builtin by_stack
+ OPT: -eva @EVA_OPTIONS@ -eva-slevel 10 -eva-mlevel 0 -eva-alloc-builtin by_stack
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc_bug_tr.c b/tests/builtins/malloc_bug_tr.c
index 98b3d323d6dc902fd725994595d35f248190f46b..c933ffe4af59ab848316ce4c7675f672d551dfc0 100644
--- a/tests/builtins/malloc_bug_tr.c
+++ b/tests/builtins/malloc_bug_tr.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@
+ OPT: -eva @EVA_OPTIONS@
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc_memexec.c b/tests/builtins/malloc_memexec.c
index cac60b4be3121fe0fe79ea701fee95860d0420a3..e02637be2be686bd338daf09baeb7eb77ae033a9 100644
--- a/tests/builtins/malloc_memexec.c
+++ b/tests/builtins/malloc_memexec.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
+ OPT: -eva @EVA_OPTIONS@ -eva-memexec -deps -inout -eva-mlevel 0
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc_multiple.c b/tests/builtins/malloc_multiple.c
index 81e2a9cc9f717679e7e98ff2047b2c5360f23bdc..337e6b4abfd0ade9566f8b3f0a2a83173ef70094 100644
--- a/tests/builtins/malloc_multiple.c
+++ b/tests/builtins/malloc_multiple.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -eva-slevel 50 -eva-mlevel 5
+ OPT: -eva @EVA_OPTIONS@ -eva-slevel 50 -eva-mlevel 5
*/
#include<stdlib.h>
#define MAX 10
diff --git a/tests/builtins/memcpy_invalid.c b/tests/builtins/memcpy_invalid.c
index cd0a7b35cf7952616fe681aa8959b5bca7feab6e..57efefd93f30951e193c70af41886d0a839962f1 100644
--- a/tests/builtins/memcpy_invalid.c
+++ b/tests/builtins/memcpy_invalid.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -journal-disable -calldeps
+ OPT: -eva @EVA_OPTIONS@ -journal-disable -calldeps
*/
/*@ assigns \result \from min, max;
diff --git a/tests/builtins/test_config b/tests/builtins/test_config
index 345f347fd4091540571356c8cf0e71c4af9fbaf8..05cba93b48eb81c1f37543a85d8dd45f9d70db8d 100644
--- a/tests/builtins/test_config
+++ b/tests/builtins/test_config
@@ -1,3 +1,2 @@
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@
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+OPT: -eva @EVA_OPTIONS@ -journal-disable -out -input -deps
diff --git a/tests/builtins/write-const.c b/tests/builtins/write-const.c
index 89dfcdd91ae135416df8d7ce0d91a279f41d1235..598d93847eb1028a9b40ef84b125dc0142775108 100644
--- a/tests/builtins/write-const.c
+++ b/tests/builtins/write-const.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -journal-disable -eva-builtins-auto -calldeps
+ OPT: -eva @EVA_OPTIONS@ -journal-disable -eva-builtins-auto -calldeps
*/
// This test verifies that writing in a memory location that may be const
diff --git a/tests/float/absorb.c b/tests/float/absorb.c
index 7a9e3cab596155c30ae2a11f31defb1f860a3eba..da1ee88e6905f8099b05f3247e9a3c960f90414d 100644
--- a/tests/float/absorb.c
+++ b/tests/float/absorb.c
@@ -1,7 +1,7 @@
/* run.config
COMMENT: run.config is intentionally not-*
EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err frama-c -no-autoload-plugins -journal-disable -save absorb.sav @PTEST_FILE@ > absorb_sav.res 2> absorb_sav.err
- EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err frama-c @FRAMA_C_PLUGINS_OPTIONS@ -load %{dep:absorb.sav} -eva @EVA_CONFIG@ -journal-disable -float-hex -save absorb.sav2 > absorb_sav2.res 2> absorb_sav2.err
+ EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err frama-c @FRAMA_C_PLUGINS_OPTIONS@ -load %{dep:absorb.sav} -eva @EVA_OPTIONS@ -journal-disable -float-hex -save absorb.sav2 > absorb_sav2.res 2> absorb_sav2.err
OPT: -load %{dep:absorb.sav2} -deps -out -input
*/
/* run.config*
diff --git a/tests/float/alarms.i b/tests/float/alarms.i
index 8d60a075054d3ed035311ea24ecb62b5f24405c9..64f4fc7965336f23ea777a9ec24034e5aff4aaf3 100644
--- a/tests/float/alarms.i
+++ b/tests/float/alarms.i
@@ -1,7 +1,7 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -warn-special-float non-finite
- OPT: -eva @EVA_CONFIG@ -warn-special-float nan
- OPT: -eva @EVA_CONFIG@ -warn-special-float none
+ OPT: -eva @EVA_OPTIONS@ -warn-special-float non-finite
+ OPT: -eva @EVA_OPTIONS@ -warn-special-float nan
+ OPT: -eva @EVA_OPTIONS@ -warn-special-float none
*/
union { long long l ; float f ; double d ; } u1, u2;
diff --git a/tests/float/builtins.c b/tests/float/builtins.c
index 1b2d53069a31c06abd0b437c3a1b388ed79672e0..102f1eff06839adc153e524164b9c1b71d2ab2a2 100644
--- a/tests/float/builtins.c
+++ b/tests/float/builtins.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -then -main main_log_exp
+ OPT: -eva @EVA_OPTIONS@ -then -main main_log_exp
*/
#include <__fc_builtin.h>
diff --git a/tests/float/cond.c b/tests/float/cond.c
index 89cc751c13707df7addc5024e5e5b5aae556091e..3d70579b34f0be1551e0c6c90fb394dcdb852d24 100644
--- a/tests/float/cond.c
+++ b/tests/float/cond.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -journal-disable -float-hex
+ OPT: -eva @EVA_OPTIONS@ -journal-disable -float-hex
*/
#include "__fc_builtin.h"
diff --git a/tests/float/const.i b/tests/float/const.i
index 9e47e611f885b5ad64dbcd15eaeb52c02cde7d27..207da778ec0b1f915d406696b365ef9d0e4541c4 100644
--- a/tests/float/const.i
+++ b/tests/float/const.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -float-hex -warn-decimal-float all -journal-disable -then -out -deps
+ OPT: -eva @EVA_OPTIONS@ -float-hex -warn-decimal-float all -journal-disable -then -out -deps
*/
typedef double mydouble;
diff --git a/tests/float/extract_bits.i b/tests/float/extract_bits.i
index 083727447193a64d526f1560c853c0a34b6c084e..552bd39549d0f7eba2d4b50a668ba74837787c2b 100644
--- a/tests/float/extract_bits.i
+++ b/tests/float/extract_bits.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -eva-slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -warn-decimal-float all
- OPT: -eva @EVA_CONFIG@ -eva-slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -warn-decimal-float all
+ OPT: -eva @EVA_OPTIONS@ -eva-slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -warn-decimal-float all
+ OPT: -eva @EVA_OPTIONS@ -eva-slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -warn-decimal-float all
*/
float f = 3.14;
diff --git a/tests/float/init_float.i b/tests/float/init_float.i
index 83d69d1336e42e0cdb64c82e99409c770eba553f..cce205f05271172d891d45e864bd19964796995b 100644
--- a/tests/float/init_float.i
+++ b/tests/float/init_float.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -journal-disable -float-normal -lib-entry
+ OPT: -eva @EVA_OPTIONS@ -journal-disable -float-normal -lib-entry
*/
typedef struct S { float y; } S;
diff --git a/tests/float/nonlin.c b/tests/float/nonlin.c
index d210fe4a31538f2594517d4668c813392b557e6b..e18380a814d7176389911ad8b7b60df97b50c720 100644
--- a/tests/float/nonlin.c
+++ b/tests/float/nonlin.c
@@ -1,10 +1,10 @@
/* run.config*
- OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 0
- OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
- OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
- OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 0
- OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
- OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_OPTIONS@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 0
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_OPTIONS@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_OPTIONS@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_OPTIONS@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 0
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_OPTIONS@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_OPTIONS@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
*/
#include "__fc_builtin.h"
diff --git a/tests/float/precise_cos_sin.c b/tests/float/precise_cos_sin.c
index f6e6f36e9077b0036d3ebd983c20cc6a0e5f4eb0..271d091d6bad8fecc362e2508e0658743bc74b15 100644
--- a/tests/float/precise_cos_sin.c
+++ b/tests/float/precise_cos_sin.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -eva-slevel 1000 -journal-disable -float-normal
+ OPT: -eva @EVA_OPTIONS@ -eva-slevel 1000 -journal-disable -float-normal
*/
#include <__fc_builtin.h>
diff --git a/tests/float/round10d.i b/tests/float/round10d.i
index 1d6ebe39de506c8e31fe6ea441ba25cfbd408cbd..ba93da532bfe9bf4c20f2ee0768f8688d0f03a63 100644
--- a/tests/float/round10d.i
+++ b/tests/float/round10d.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -float-normal -journal-disable -eva-no-results
+ OPT: -eva @EVA_OPTIONS@ -float-normal -journal-disable -eva-no-results
*/
int main()
diff --git a/tests/float/some.c b/tests/float/some.c
index 8eb3f38ea73da66b5c52a6779382e274a9a6a3ee..70b34621e966dd90d38b879e5835ae3541bbf1fd 100644
--- a/tests/float/some.c
+++ b/tests/float/some.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva-show-slevel 10 -eva-slevel 100 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double -DN=55" -float-normal -journal-disable -eva-no-results
- OPT: -eva-slevel 100 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float -DN=26" -float-normal -journal-disable -eva-no-results
+ OPT: -eva-show-slevel 10 -eva-slevel 100 -eva @EVA_OPTIONS@ -cpp-extra-args="-DFLOAT=double -DN=55" -float-normal -journal-disable -eva-no-results
+ OPT: -eva-slevel 100 -eva @EVA_OPTIONS@ -cpp-extra-args="-DFLOAT=float -DN=26" -float-normal -journal-disable -eva-no-results
*/
FLOAT t[N] = { 1. } ;
diff --git a/tests/float/special_floats.c b/tests/float/special_floats.c
index 1e07cd3a6ba385e0b3eec0bda2eb0aa1381200d3..67bd40b60be95058ed1e749b94924cf26a3e753f 100644
--- a/tests/float/special_floats.c
+++ b/tests/float/special_floats.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -warn-special-float none
+ OPT: -eva @EVA_OPTIONS@ -warn-special-float none
*/
/* Tests on special float values NaN and infinites. */
diff --git a/tests/impact/test_config b/tests/impact/test_config
index 39d00a53e2544038b045de3df9691cb4b61e5f6d..c0e7feda3b59d228d66ade073068f424bd328b86 100644
--- a/tests/impact/test_config
+++ b/tests/impact/test_config
@@ -1,2 +1,2 @@
-PLUGIN: impact @EVA_PLUGINS@
+PLUGIN: impact @EVA_CONFIG@
OPT: -journal-disable -impact-print @EVA_OPTIONS@
diff --git a/tests/journal/control.i b/tests/journal/control.i
index 0830044b07ebffc8d9936ce0d3e143aee547af5f..0166aadcd1e5fe9bf10d52000de2285713a54c0c 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 (frama-c @FRAMA_C_PLUGINS_OPTIONS@ -journal-enable -check -eva -deps -out @EVA_CONFIG@ -main f -journal-name control_journal.ml control.i && cp control_journal.ml control_journal_bis.ml) > /dev/null 2> /dev/null
+ EXECNOW: BIN control_journal.ml BIN control_journal_bis.ml (frama-c @FRAMA_C_PLUGINS_OPTIONS@ -journal-enable -check -eva -deps -out @EVA_OPTIONS@ -main f -journal-name control_journal.ml control.i && cp control_journal.ml control_journal_bis.ml) > /dev/null 2> /dev/null
CMD: @frama-c@
OPT: -load-script %{dep:control_journal.ml} -journal-disable
CMD: @frama-c@
diff --git a/tests/journal/control2.c b/tests/journal/control2.c
index f5c82393b8e5ffd2ffc1f561449d0aacdcb9f803..c4676ac29be6ee54c6c1ef6f79c99dbec40c7fed 100644
--- a/tests/journal/control2.c
+++ b/tests/journal/control2.c
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: BIN control_journal2.ml frama-c @FRAMA_C_PLUGINS_OPTIONS@ -journal-enable -eva -deps -out -main f -journal-name control_journal2.ml @PTEST_FILE@ > /dev/null 2> /dev/null
EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml frama-c @FRAMA_C_PLUGINS_OPTIONS@ -journal-enable -load-script %{dep:control_journal2.ml} -lib-entry -journal-name control_journal_next2.ml @PTEST_FILE@ > control2_sav.res 2> control2_sav.err
- PLUGIN: callgraph @EVA_PLUGINS@
+ PLUGIN: callgraph @EVA_CONFIG@
OPT: -load-script %{dep:control_journal_next2.ml}
*/
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 9d3006bde7eb89d22fe4aff4fc21c88349c3ed6d..1f063870bdde9543b633a1b53f4f137fc9179d59 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: sparecode @EVA_PLUGINS@
+ PLUGIN: sparecode @EVA_CONFIG@
CMXS: @PTEST_NAME@
EXECNOW: BIN intra_journal.ml frama-c -eva-show-progress -no-autoload-plugins -load-plugin from,inout,eva,scope,variadic,sparecode -load-module %{dep:@PTEST_NAME@.cmxs} -journal-enable -journal-name intra_journal.ml @PTEST_NAME@.i > /dev/null 2> /dev/null
CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs}
diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index e11d52b0330129622247b44d9725dc2288d52ec5..0a63b6c3c76a58c550554e41fb1e32a460444168 100644
--- a/tests/libc/coverage.c
+++ b/tests/libc/coverage.c
@@ -1,5 +1,5 @@
/* run.config*
- PLUGIN: metrics @EVA_PLUGINS@
+ PLUGIN: metrics @EVA_CONFIG@
OPT: -eva-no-builtins-auto @EVA_OPTIONS@ %{read:../../syntax/framac_share_path}/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
*/
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 3279d4aa85c369135c894ea8e6157d9101f0a3f2..116627e871111c0fba047d5c60b6ee16e1812273 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -4,8 +4,8 @@
CMXS: check_parsing_individual_headers
CMXS: check_libc_anonymous_tags
CMXS: check_compliance
- PLUGIN: metrics @EVA_PLUGINS@
- OPT: -load-module %{dep:check_libc_naming_conventions.cmxs} -print -cpp-extra-args='-nostdinc' -metrics -metrics-libc -load-module %{dep:check_const.cmxs} -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
+ PLUGIN: metrics @EVA_CONFIG@
+ OPT: -load-module %{dep:check_libc_naming_conventions.cmxs} -print -cpp-extra-args='-nostdinc' -metrics -metrics-libc -load-module %{dep:check_const.cmxs} -eva @EVA_OPTIONS@ -then -lib-entry -no-print -metrics-no-libc
OPT: -print -print-libc
OPT: -load-module %{dep:check_parsing_individual_headers.cmxs}
OPT: -load-module %{dep:check_libc_anonymous_tags.cmxs}
diff --git a/tests/libc/test_config b/tests/libc/test_config
index cf5c5bb18359425ba47e530ac8c06c936f24d7e8..fca40f274632be2a48598c781597677a7db02415 100644
--- a/tests/libc/test_config
+++ b/tests/libc/test_config
@@ -1 +1 @@
-OPT: -eva @EVA_CONFIG@ -cpp-extra-args='-nostdinc -Ishare/libc'
+OPT: -eva @EVA_OPTIONS@ -cpp-extra-args='-nostdinc -Ishare/libc'
diff --git a/tests/misc/add_assigns.i b/tests/misc/add_assigns.i
index 13b86591a9bf84f8a29254ab5041fdbf4204fb4d..e520ee7eb446c474d6aa868fa2cc0fde537d64e4 100644
--- a/tests/misc/add_assigns.i
+++ b/tests/misc/add_assigns.i
@@ -1,5 +1,5 @@
/* run.config
-PLUGIN: report @EVA_PLUGINS@
+PLUGIN: report @EVA_CONFIG@
MODULE: @PTEST_NAME@.cmxs
OPT: -then -report -then -print
*/
diff --git a/tests/misc/bts0541.c b/tests/misc/bts0541.c
index 6bbabaaa30cadda796dfc7d69e53074fb4058368..213d4e2cd99292ebf6ed1ed0a9c9845529b2e67c 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_CONFIG@
+ OPT: -pp-annot -cpp-extra-args="-I./share/libc" -pp-annot -eva @EVA_OPTIONS@
*/
#include <stdbool.h>
diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i
index 2df285ccb7dfa9d67234ee0fffc987c67b3273d4..8313408099af7b17277f00cc4db068c04e9a7a86 100644
--- a/tests/misc/bts1347.i
+++ b/tests/misc/bts1347.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: report @EVA_PLUGINS@
+ PLUGIN: report @EVA_CONFIG@
MODULE: @PTEST_NAME@.cmxs
OPT: @EVA_OPTIONS@ -then -report
*/
diff --git a/tests/misc/issue109.i b/tests/misc/issue109.i
index 790aa603d9df3f695be6975ded0a8f78363be1dc..1f23c8fe05c28b81b37f98a972b56a80ba33d02e 100644
--- a/tests/misc/issue109.i
+++ b/tests/misc/issue109.i
@@ -1,6 +1,6 @@
/* run.config
MODULE: @PTEST_NAME@.cmxs
- OPT: -eva @EVA_CONFIG@ -eva-slevel-function main:10
+ OPT: -eva @EVA_OPTIONS@ -eva-slevel-function main:10
*/
void main() {
int i, j = 0;
diff --git a/tests/misc/log_twice.i b/tests/misc/log_twice.i
index dc2306c1c6e9a5e6121d9c53e6e5a670609f6af4..e97f81ad8792312f7c82f453d1fa5d7e9ee6a8c5 100644
--- a/tests/misc/log_twice.i
+++ b/tests/misc/log_twice.i
@@ -1,6 +1,6 @@
/* run.config
MODULE: @PTEST_NAME@.cmxs
- OPT: @EVA_CONFIG@
+ OPT: @EVA_OPTIONS@
*/
int* f() {
diff --git a/tests/misc/obfuscate.c b/tests/misc/obfuscate.c
index d28ccfb42f935fa60a5de15fad7ce6d072e7d254..3efb19fac6fe64657cd6cc69a64288e7719ac206 100644
--- a/tests/misc/obfuscate.c
+++ b/tests/misc/obfuscate.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: obfuscator @EVA_PLUGINS@
+ PLUGIN: obfuscator @EVA_CONFIG@
OPT: -obfuscate
*/
int my_var = 0;
diff --git a/tests/misc/widen_hints.c b/tests/misc/widen_hints.c
index e4f063807c12972b188952fa735a10024d17c844..1ececc21c8456f9960a66163bf18bc872214899b 100644
--- a/tests/misc/widen_hints.c
+++ b/tests/misc/widen_hints.c
@@ -1,8 +1,8 @@
/* run.config
- 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@ -eva-slevel 1 -eva-msg-key widen-hints
- OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DALLGLOBAL -eva-msg-key widen-hints
+ OPT: -eva @EVA_OPTIONS@ -cpp-extra-args=-DSYNTAX_ERRORS -kernel-warn-key=annot-error=active
+ OPT: -eva @EVA_OPTIONS@ -cpp-extra-args=-DNONCONST
+ OPT: -eva @EVA_OPTIONS@ -eva-slevel 1 -eva-msg-key widen-hints
+ OPT: -eva @EVA_OPTIONS@ -cpp-extra-args=-DALLGLOBAL -eva-msg-key widen-hints
*/
#define N 2
diff --git a/tests/occurrence/test_config b/tests/occurrence/test_config
index 029a71e6518323c3e32e2950e023ee1bf8687253..f68b112eccd0e3a541bae9a937c28569b2a732f7 100644
--- a/tests/occurrence/test_config
+++ b/tests/occurrence/test_config
@@ -1,2 +1,2 @@
-PLUGIN: occurrence @EVA_PLUGINS@
+PLUGIN: occurrence @EVA_CONFIG@
STDOPT: -"-eva" -"-out" -"-input" -"-deps" +"-occurrence-verbose 1"
diff --git a/tests/pdg/bts1194.c b/tests/pdg/bts1194.c
index aaa06aacad1c5038696f57e95c6f557179be2f34..3a8043fdba9906c389defb22b841e23d207431b6 100644
--- a/tests/pdg/bts1194.c
+++ b/tests/pdg/bts1194.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: slicing @EVA_PLUGINS@
+ PLUGIN: slicing @EVA_CONFIG@
STDOPT: +"-eva -inout -pdg -calldeps -deps -then -slice-return main -then-last -print @EVA_OPTIONS@"
*/
diff --git a/tests/pdg/test_config b/tests/pdg/test_config
index 78c7757cadf8d143e6823856234b4ab43b1a3839..42a9ea00fb225a1a746d93560735058a8410ad5f 100644
--- a/tests/pdg/test_config
+++ b/tests/pdg/test_config
@@ -1,2 +1,2 @@
-PLUGIN: pdg @EVA_PLUGINS@
+PLUGIN: pdg @EVA_CONFIG@
OPT: -journal-disable @EVA_OPTIONS@ -pdg-print -pdg-verbose 2
diff --git a/tests/rte/test_config b/tests/rte/test_config
index 60080e46918d03b8587ae6b09528301f66b0ae50..d265e69bf9fe0845ca3de4103ff2a4cd25ec1fe6 100644
--- a/tests/rte/test_config
+++ b/tests/rte/test_config
@@ -1 +1 @@
-PLUGIN: rtegen @EVA_PLUGINS@
+PLUGIN: rtegen @EVA_CONFIG@
diff --git a/tests/rte/value_rte.c b/tests/rte/value_rte.c
index 186136b4a704446ee7e2c38e9d059310ada50207..d614f1cd9aaabce832282232cf57092ed74e8b5e 100644
--- a/tests/rte/value_rte.c
+++ b/tests/rte/value_rte.c
@@ -1,5 +1,5 @@
/* run.config
-PLUGIN: report @EVA_PLUGINS@
+PLUGIN: report @EVA_CONFIG@
OPT: -rte -then -eva @EVA_OPTIONS@ -then -report
*/
diff --git a/tests/saveload/load_one.i b/tests/saveload/load_one.i
index de48930209eb6e91e10defb904cf264e10ffba66..27120f1a347b259be251ac67e236e5272f869c07 100644
--- a/tests/saveload/load_one.i
+++ b/tests/saveload/load_one.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: sparecode @EVA_PLUGINS@
+ PLUGIN: sparecode @EVA_CONFIG@
MODULE: @PTEST_NAME@.cmxs
STDOPT:
*/
diff --git a/tests/scope/bts383.c b/tests/scope/bts383.c
index b2b410d23c770ed15c41224b60833a4bb40a57cc..253a960f6db0e7b6e0a5283bb2646f97a24673b4 100644
--- a/tests/scope/bts383.c
+++ b/tests/scope/bts383.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -eva @EVA_CONFIG@ -print -journal-disable -scope-verbose 1 -eva-remove-redundant-alarms -eva-context-width 3
+ OPT: -eva @EVA_OPTIONS@ -print -journal-disable -scope-verbose 1 -eva-remove-redundant-alarms -eva-context-width 3
*/
/*
echo '!Db.Scope.check_asserts();;' \
diff --git a/tests/scope/no-effect.i b/tests/scope/no-effect.i
index 7b75f9e1d9f28d1b4893aa62a97fa4c8ca2eb3a7..011a3fe5dad631e7b9b0f9e03c0557555bb98d42 100644
--- a/tests/scope/no-effect.i
+++ b/tests/scope/no-effect.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: @EVA_CONFIG@ -eva -print -journal-disable -scope-verbose 1 -eva-remove-redundant-alarms
+ OPT: @EVA_OPTIONS@ -eva -print -journal-disable -scope-verbose 1 -eva-remove-redundant-alarms
*/
typedef struct {
diff --git a/tests/scope/scope.c b/tests/scope/scope.c
index a8902199641b023a6750635832d169e023aa9af6..8a7d1df5d6f9f37ab783f91b5cb3f6cf8f0942ed 100644
--- a/tests/scope/scope.c
+++ b/tests/scope/scope.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: -eva @EVA_CONFIG@ -main f -journal-disable
- OPT: -eva @EVA_CONFIG@ -main f2 -journal-disable
- OPT: -eva @EVA_CONFIG@ -main loop -journal-disable
+ OPT: -eva @EVA_OPTIONS@ -main f -journal-disable
+ OPT: -eva @EVA_OPTIONS@ -main f2 -journal-disable
+ OPT: -eva @EVA_OPTIONS@ -main loop -journal-disable
*/
/*
* bin/viewer.byte -main f scope.c -eva
diff --git a/tests/scope/zones.c b/tests/scope/zones.c
index 80fc7e30553dbf463b58bf27048435c76d607838..7b3d2161b05f23f52f8bf294f528db68c78237d2 100644
--- a/tests/scope/zones.c
+++ b/tests/scope/zones.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_PLUGINS@ pdg
+ PLUGIN: @EVA_CONFIG@ pdg
CMXS: @PTEST_NAME@
OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -eva @EVA_OPTIONS@ -journal-disable
*/
diff --git a/tests/slicing/test_config b/tests/slicing/test_config
index 2a8603f22a83a30f9e73a12abb85510c4f212781..fff12f16b671297f812a8f6701b214a3e45ed9b8 100644
--- a/tests/slicing/test_config
+++ b/tests/slicing/test_config
@@ -1,2 +1,2 @@
-PLUGIN: slicing @EVA_PLUGINS@
+PLUGIN: slicing @EVA_CONFIG@
OPT: @EVA_OPTIONS@
diff --git a/tests/spec/array_typedef.c b/tests/spec/array_typedef.c
index a8273f598146e1ddb45647df4ec7477d47f347f9..7882dfda13967c35fcfc11f06c22a791ad95ea42 100644
--- a/tests/spec/array_typedef.c
+++ b/tests/spec/array_typedef.c
@@ -1,5 +1,5 @@
/*run.config
- PLUGIN: @EVA_PLUGINS@
+ PLUGIN: @EVA_CONFIG@
OPT: -print -eva @EVA_OPTIONS@ -journal-disable
*/
#define IP_FIELD 4
diff --git a/tests/spec/assigns_result.i b/tests/spec/assigns_result.i
index bfde0dde8bfeafeac8e63a972479dfcc80b2e97e..134947f6cd5b6b73493037c82f51020c507b2caa 100644
--- a/tests/spec/assigns_result.i
+++ b/tests/spec/assigns_result.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_PLUGINS@
+ PLUGIN: @EVA_CONFIG@
STDOPT: +"-deps @EVA_OPTIONS@"
*/
int X,Y;
diff --git a/tests/spec/assigns_void.c b/tests/spec/assigns_void.c
index a93209867cbbc10b8f6a74157690640881a02ca9..ba4f8a4ac52f3f6b16fed4285d3640e3486f783a 100644
--- a/tests/spec/assigns_void.c
+++ b/tests/spec/assigns_void.c
@@ -1,7 +1,7 @@
/* run.config
OPT: -print -journal-disable -kernel-warn-key=annot-error=active
- PLUGIN: @EVA_PLUGINS@
- OPT: -eva @EVA_CONFIG@ -main g -print -no-annot -journal-disable
+ PLUGIN: @EVA_CONFIG@
+ OPT: -eva @EVA_OPTIONS@ -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 e130481efd9d88ce982877e44d3abc01814783a3..30c5049425710c4c550b9119068fb2c46cba5278 100644
--- a/tests/spec/behavior_assert.c
+++ b/tests/spec/behavior_assert.c
@@ -1,7 +1,7 @@
/* run.config
- PLUGIN: @EVA_PLUGINS@
- OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable -lib-entry
- OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable
+ PLUGIN: @EVA_CONFIG@
+ OPT: -eva @EVA_OPTIONS@ -deps -out -input -journal-disable -lib-entry
+ OPT: -eva @EVA_OPTIONS@ -deps -out -input -journal-disable
*/
int e;
diff --git a/tests/spec/default_assigns_bts0966.i b/tests/spec/default_assigns_bts0966.i
index 0bffe80560eef462f8bf954d9093a8b8d854ed30..c473d0d55d851272fd54a6f74679b71ce4ae0a47 100644
--- a/tests/spec/default_assigns_bts0966.i
+++ b/tests/spec/default_assigns_bts0966.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_PLUGINS@
+ PLUGIN: @EVA_CONFIG@
OPT: -eva -print
*/
int auto_states[4] ; // = { 1 , 0 , 0, 0 };
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 0068ae1099a05428a94a14047f15735fcb219756..23ab2c814494dc31ce1740bae6018d8e7954ca94 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,5 +1,5 @@
/* run.config
-PLUGIN: wp @EVA_PLUGINS@
+PLUGIN: wp @EVA_CONFIG@
OPT: -wp -wp-prover qed -wp-msg-key shell
OPT: -eva -eva-use-spec f
OPT: -print
diff --git a/tests/spec/logic_def.c b/tests/spec/logic_def.c
index 8448756e44a5693e646a07608132edc247187e26..f309563f6bf1f7fd46e46fb1d3bb0aa4358fb2af 100644
--- a/tests/spec/logic_def.c
+++ b/tests/spec/logic_def.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_PLUGINS@
+ PLUGIN: @EVA_CONFIG@
STDOPT: +"-eva -eva-verbose 2"
*/
//@ logic integer foo(int x) = x + 2 ;
diff --git a/tests/spec/preprocess.c b/tests/spec/preprocess.c
index f0fffe879411fdcf440017be7e49ce147f2076af..d22f2b661df4018473b9c1c0d9962cfa37c624d1 100644
--- a/tests/spec/preprocess.c
+++ b/tests/spec/preprocess.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_PLUGINS@
+ PLUGIN: @EVA_CONFIG@
DEPS: preprocess.h
OPT: -eva @EVA_OPTIONS@ -journal-disable -print
*/
diff --git a/tests/spec/shifts.c b/tests/spec/shifts.c
index af132b55019639d055ded6f3464464409f32d442..96e4eb6e8922a902b10d9f5986a5a0927f5d176b 100644
--- a/tests/spec/shifts.c
+++ b/tests/spec/shifts.c
@@ -1,6 +1,6 @@
/* run.config
- PLUGIN: @EVA_PLUGINS@
- OPT: -eva @EVA_CONFIG@ -deps -journal-disable
+ PLUGIN: @EVA_CONFIG@
+ OPT: -eva @EVA_OPTIONS@ -deps -journal-disable
*/
int e;
diff --git a/tests/spec/statement_behavior.c b/tests/spec/statement_behavior.c
index 02551271d9e7eb7da938ec7026e539693397beb3..2e462bd59fd128124fba41e5e5dec1cc788f1f3e 100644
--- a/tests/spec/statement_behavior.c
+++ b/tests/spec/statement_behavior.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_PLUGINS@
+ PLUGIN: @EVA_CONFIG@
OPT: -eva @EVA_OPTIONS@ -inout -journal-disable
*/
diff --git a/tests/syntax/copy_visitor.i b/tests/syntax/copy_visitor.i
index 2f475d79ae7a5ebeaf572e79e97e4b5f533cc833..be3439277c20943007a6e3dc24d68e1a4027f92e 100644
--- a/tests/syntax/copy_visitor.i
+++ b/tests/syntax/copy_visitor.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-copy -eva @EVA_CONFIG@"
+ STDOPT: +"-copy -eva @EVA_OPTIONS@"
*/
struct S {
int a;
diff --git a/tests/syntax/extern_init.i b/tests/syntax/extern_init.i
index 447af8e54b9cc316fcda4cadea36afe0a5be7da8..43e6f42f933ced55d913dad07968ab0def323d40 100644
--- a/tests/syntax/extern_init.i
+++ b/tests/syntax/extern_init.i
@@ -1,6 +1,6 @@
/* run.config
-OPT: %{dep:@PTEST_NAME@_1.i} %{dep:@PTEST_NAME@_2.i} -eva @EVA_CONFIG@
-OPT: %{dep:@PTEST_NAME@_2.i} %{dep:@PTEST_NAME@_1.i} -eva @EVA_CONFIG@
+OPT: %{dep:@PTEST_NAME@_1.i} %{dep:@PTEST_NAME@_2.i} -eva @EVA_OPTIONS@
+OPT: %{dep:@PTEST_NAME@_2.i} %{dep:@PTEST_NAME@_1.i} -eva @EVA_OPTIONS@
*/
extern int a[] ;
diff --git a/tests/syntax/unroll_labels.i b/tests/syntax/unroll_labels.i
index 66da8b7cf4882b0214a9cc46294e20ff7f81668b..ba2041166699e1bb4864be9510c0af3338f82fb3 100644
--- a/tests/syntax/unroll_labels.i
+++ b/tests/syntax/unroll_labels.i
@@ -1,6 +1,6 @@
/* run.config
- STDOPT: +"-eva @EVA_CONFIG@"
- STDOPT: +"-eva @EVA_CONFIG@ -main main2 -eva-slevel 3"
+ STDOPT: +"-eva @EVA_OPTIONS@"
+ STDOPT: +"-eva @EVA_OPTIONS@ -main main2 -eva-slevel 3"
*/
enum { SIX = 6 } ;
volatile foo;
diff --git a/tests/syntax/unroll_visit.i b/tests/syntax/unroll_visit.i
index 38d55c380b64b1be5bc5017806f5f0f462ef59e8..a1cfdabf081733b683ede992e6b7f13f8b46b181 100644
--- a/tests/syntax/unroll_visit.i
+++ b/tests/syntax/unroll_visit.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-eva @EVA_CONFIG@ -deps -out -input -deps"
+ STDOPT: +"-eva @EVA_OPTIONS@ -deps -out -input -deps"
*/
void main() {
/*@ loop pragma UNROLL 2; */
diff --git a/tests/test_config b/tests/test_config
index fecc43ece3426f31ed6d00453cc984e76e83e3ce..5a534c7ec2d54b5f4f53205bcf34226bf35bc316 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,5 +1,4 @@
-MACRO: EVA_PLUGINS from inout eva scope variadic
+MACRO: EVA_CONFIG from inout eva scope variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
-MACRO: EVA_CONFIG @EVA_OPTIONS@
-PLUGIN: @EVA_PLUGINS@
+PLUGIN: @EVA_CONFIG@
OPT: -eva @EVA_OPTIONS@ -journal-disable -out -input -deps
diff --git a/tests/value/align_char_array.c b/tests/value/align_char_array.c
index de692f2f709f3533998e31d902afee308ad011df..98d2a1d84b5e75eb482b49e6d7e99ddc15098f2e 100644
--- a/tests/value/align_char_array.c
+++ b/tests/value/align_char_array.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -cpp-extra-args="-DPTEST" -journal-disable
*/
diff --git a/tests/value/array_initializer.i b/tests/value/array_initializer.i
index 04029accd9cbbc52b82684a435bb807b5c29d50a..9ba8114198b9f722ae7b9b37afcb0aae7237807f 100644
--- a/tests/value/array_initializer.i
+++ b/tests/value/array_initializer.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals maybe
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -then -eva-initialization-padding-globals maybe
*/
int t[5] = { [2] = 3 };
diff --git a/tests/value/array_zero_length.i b/tests/value/array_zero_length.i
index f84a4ebf84a90dfca79e584bfc02975497a704cf..a57db72764c901a14ac6bd8363ad7ea64ab0d68d 100644
--- a/tests/value/array_zero_length.i
+++ b/tests/value/array_zero_length.i
@@ -1,7 +1,7 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -journal-disable -machdep gcc_x86_32
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable -machdep gcc_x86_32
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -journal-disable -machdep gcc_x86_32
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -lib-entry -journal-disable -machdep gcc_x86_32
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -lib-entry -journal-disable
*/
char T[];
diff --git a/tests/value/base_addr_offset_block_length.i b/tests/value/base_addr_offset_block_length.i
index b3aad4d14b7a622e69f1e547cd8f84ef8434dfbd..df95d296e8a67ed4071577cecc5790c43a9514cd 100644
--- a/tests/value/base_addr_offset_block_length.i
+++ b/tests/value/base_addr_offset_block_length.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -eva-context-width 3 -then -eva-slevel 3
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -eva-context-width 3 -then -eva-slevel 3
*/
diff --git a/tests/value/big_lib_entry.i b/tests/value/big_lib_entry.i
index 0c2770eab0fefe3254629223350644dbbf8493e2..6118abf10cec2f6e968daf4132b2da3026c50201 100644
--- a/tests/value/big_lib_entry.i
+++ b/tests/value/big_lib_entry.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -eva-context-width 4 -eva-initialization-padding-globals no
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -lib-entry -eva-context-width 4 -eva-initialization-padding-globals no
*/
typedef struct {
diff --git a/tests/value/bitfield_longlong.c b/tests/value/bitfield_longlong.c
index c2bdb9d6234e025769ac59c269deac5d6f03ec7e..1f486c7ab6d46dff54d9eb897ef465cd3a35926a 100644
--- a/tests/value/bitfield_longlong.c
+++ b/tests/value/bitfield_longlong.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-Dprintf=Frama_C_show_each" -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -cpp-extra-args="-Dprintf=Frama_C_show_each" -journal-disable
*/
struct X50 {
long long int z:50;
diff --git a/tests/value/bts1306.i b/tests/value/bts1306.i
index 81f9cc8f329ead372748ebd5eea97821b99bc0bd..8ce8ae82294a44985a042831d7d00ff82473a757 100644
--- a/tests/value/bts1306.i
+++ b/tests/value/bts1306.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -constfold -eva-slevel 0 -eva @EVA_CONFIG@ -print -then -eva-slevel 10 -eva -print
+ OPT: -no-autoload-plugins -load-module from,inout,eva -constfold -eva-slevel 0 -eva @EVA_OPTIONS@ -print -then -eva-slevel 10 -eva -print
*/
void g(double x) { double y= x*x; }
diff --git a/tests/value/case_analysis.i b/tests/value/case_analysis.i
index 40be501257b9f1b5edca5e3a305db685148deb04..ec832a708da76f9a461bb3a52a5e8bcd89b7c88b 100644
--- a/tests/value/case_analysis.i
+++ b/tests/value/case_analysis.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -eva-slevel 30 -journal-disable -float-normal
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -eva-slevel 30 -journal-disable -float-normal
*/
diff --git a/tests/value/cond_integer_cast_of_float.i b/tests/value/cond_integer_cast_of_float.i
index 9d1350ea671348d2759998a9ec5b3f9a2473455b..00f6714bff5ef640926f9c0ae38f82db1f44a76d 100644
--- a/tests/value/cond_integer_cast_of_float.i
+++ b/tests/value/cond_integer_cast_of_float.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -eva-no-results -then -float-hex -main mainbis
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_OPTIONS@ -eva-no-results -then -float-hex -main mainbis
*/
typedef double D;
typedef float F;
diff --git a/tests/value/const_typedef.i b/tests/value/const_typedef.i
index d9f7f3677ca57b9fe40bdc4bfe5b83857a99bc2b..a6432e9474afed6908c4fb7d287f493c227c1503 100644
--- a/tests/value/const_typedef.i
+++ b/tests/value/const_typedef.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -print -then -eva @EVA_CONFIG@ -lib-entry -no-print
+ OPT: -no-autoload-plugins -load-module inout,eva -print -then -eva @EVA_OPTIONS@ -lib-entry -no-print
*/
typedef int INT[3][3];
diff --git a/tests/value/constarraystructlibentry.i b/tests/value/constarraystructlibentry.i
index 96049bcde852de75c8e5efabe6c11fa5d73aca84..b311d4d4c850882f893cdc1786d8ca28cddb43b6 100644
--- a/tests/value/constarraystructlibentry.i
+++ b/tests/value/constarraystructlibentry.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -eva-initialization-padding-globals yes -then -eva-initialization-padding-globals no
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -lib-entry -eva-initialization-padding-globals yes -then -eva-initialization-padding-globals no
*/
const int t[] = { 1, 2, 3, 4, 5 } ;
diff --git a/tests/value/context_free.i b/tests/value/context_free.i
index 19c6fe292ad444d74ab88ef5c0a76fd4c776d76c..581cf60d62160fb42e94d34a92ed41f47677f7f6 100644
--- a/tests/value/context_free.i
+++ b/tests/value/context_free.i
@@ -1,6 +1,6 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -main f -absolute-valid-range 0x200-0x199 -eva-msg-key initial-state -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -lib-entry -main f -absolute-valid-range 0x200-0x199 -eva-msg-key initial-state -journal-disable
*/
diff --git a/tests/value/dead_inout.i b/tests/value/dead_inout.i
index 8cf0b0271e64bd950206a33e0f67093c1e6bc6c2..8385ed56381c4677db9f74ef9492adad6ebf3d16 100644
--- a/tests/value/dead_inout.i
+++ b/tests/value/dead_inout.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -out -input -inout -inout -main main_all
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_OPTIONS@ -out -input -inout -inout -main main_all
*/
// This tests a potential imprecision with the computation of input and outputs if one forgets to test that a statement is dead
diff --git a/tests/value/div.i b/tests/value/div.i
index 3ac38b6068dae4271ea190752b7b1efcac5fe878..bbbc25443de39eb609cf8d697afc2f64d2c0789b 100644
--- a/tests/value/div.i
+++ b/tests/value/div.i
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-load-module scope -eva-remove-redundant-alarms"
- OPT: -no-autoload-plugins -load-module eva,inout -rte -then -eva @EVA_CONFIG@
+ OPT: -no-autoload-plugins -load-module eva,inout -rte -then -eva @EVA_OPTIONS@
*/
int X,Y,Z1,Z2,T,U1,U2,V,W1,W2;
int a,b,d1,d2,d0,e;
diff --git a/tests/value/fptr.i b/tests/value/fptr.i
index 88daeab0630cbe97a44d8fb52def872d8d5f4bdd..d09fb01b4a839d613a608014a69370ec3bcd0ff6 100644
--- a/tests/value/fptr.i
+++ b/tests/value/fptr.i
@@ -1,7 +1,7 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -journal-disable -then -deps -out
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main main_uninit -journal-disable -then -deps -out
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_OPTIONS@ -journal-disable -then -deps -out
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_OPTIONS@ -main main_uninit -journal-disable -then -deps -out
*/
int R=77; volatile int v; int n;
diff --git a/tests/value/incorrect_reduce_expr.i b/tests/value/incorrect_reduce_expr.i
index 0c7f22f6219efabde4f3dfd99e6eb8e74a44315c..91a2bad26a6c27062132c3bfa188a274dd4b4806 100644
--- a/tests/value/incorrect_reduce_expr.i
+++ b/tests/value/incorrect_reduce_expr.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -absolute-valid-range 32-36
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -absolute-valid-range 32-36
*/
char t[5];
diff --git a/tests/value/inout.i b/tests/value/inout.i
index 2e00e3273ace9c6e10ae5ed5e3e74e4578348b9f..b3fdc348ff3aff661ae29027488951104379ca22 100644
--- a/tests/value/inout.i
+++ b/tests/value/inout.i
@@ -1,10 +1,10 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main inout_11_0 -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main inout_11_3 -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main never_terminate -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main may_not_terminate -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main call_may_not_terminate -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_OPTIONS@ -inout -deps -main inout_11_0 -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_OPTIONS@ -inout -deps -main inout_11_3 -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_OPTIONS@ -inout -deps -main never_terminate -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_OPTIONS@ -inout -deps -main may_not_terminate -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_OPTIONS@ -inout -deps -main call_may_not_terminate -journal-disable
*/
int Xt, Xs, Xs_I, Ys, Ys_I, Z, I;
diff --git a/tests/value/inout_formals.i b/tests/value/inout_formals.i
index 96883b0436b0ba18a4cf72be2e6d664b4aabe98e..bed7b5a38bd3f1067cd879604a84036a15a7b80a 100644
--- a/tests/value/inout_formals.i
+++ b/tests/value/inout_formals.i
@@ -1,5 +1,5 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -input-with-formals -inout-with-formals
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_OPTIONS@ -inout -input-with-formals -inout-with-formals
*/
int x, y;
diff --git a/tests/value/inout_proto.i b/tests/value/inout_proto.i
index 977b1591fed06b16f136349a8e77f54120595216..7a0e12c1124516b1f9df491e96cb4d143ac9474b 100644
--- a/tests/value/inout_proto.i
+++ b/tests/value/inout_proto.i
@@ -1,5 +1,5 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -input-with-formals -inout-with-formals -main main_main
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_OPTIONS@ -inout -input-with-formals -inout-with-formals -main main_main
*/
typedef unsigned char BYTE;
diff --git a/tests/value/limits.c b/tests/value/limits.c
index 965d689d1099207749cd4e1caab99964a83a2d44..d528d6ac4e7d54a480a8efdcd4a20ef0c073c623 100644
--- a/tests/value/limits.c
+++ b/tests/value/limits.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -warn-signed-overflow
*/
#include <limits.h>
diff --git a/tests/value/logic_ptr_cast.i b/tests/value/logic_ptr_cast.i
index 64eb43489d69f0c135df3a29dda3d8eee22bb6c2..1d4a9e44fa07693800da14a2c51b47c6839eed17 100644
--- a/tests/value/logic_ptr_cast.i
+++ b/tests/value/logic_ptr_cast.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -print -journal-disable -eva-no-results
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_OPTIONS@ -print -journal-disable -eva-no-results
*/
int *p;
int t[90];
diff --git a/tests/value/loop_test.i b/tests/value/loop_test.i
index 6b1e166139c0aad1abf2f61f4b99233d4639dba5..9037943fb0e551974d54232d9fe9ea87b3d27d1b 100644
--- a/tests/value/loop_test.i
+++ b/tests/value/loop_test.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main test_onzes -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main test_cent_onzes -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_OPTIONS@ -main test_onzes -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_OPTIONS@ -main test_cent_onzes -journal-disable
*/
diff --git a/tests/value/loop_wvar.i b/tests/value/loop_wvar.i
index 341e446a0ad758d60a6c278b8609dc472a3ccf8b..d07c4120598d3d11996a21ab5ac28e8e11f9735f 100644
--- a/tests/value/loop_wvar.i
+++ b/tests/value/loop_wvar.i
@@ -1,8 +1,8 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -no-annot -eva @EVA_CONFIG@ -then -kernel-warn-key=annot-error=active -annot -eva -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout,eva -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main3 -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main_err1 -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main_err2 -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -no-annot -eva @EVA_OPTIONS@ -then -kernel-warn-key=annot-error=active -annot -eva -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -kernel-warn-key=annot-error=active -eva @EVA_OPTIONS@ -main main3 -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @EVA_OPTIONS@ -main main_err1 -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @EVA_OPTIONS@ -main main_err2 -journal-disable
*/
diff --git a/tests/value/loopinv.c b/tests/value/loopinv.c
index 26f3a1e37b27e5b099b572084544f16092a6d911..3e1e308fb65cd9ae11193672b7b3231cdab1fe88 100644
--- a/tests/value/loopinv.c
+++ b/tests/value/loopinv.c
@@ -1,5 +1,5 @@
/* run.config*
-OPT: @EVA_CONFIG@ -no-autoload-plugins -load-module from,inout,eva,report -eva-slevel-function main2:20 -pp-annot -eva -then -report
+OPT: @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,report -eva-slevel-function main2:20 -pp-annot -eva -then -report
*/
/*@ requires valid: \valid(&t[0..s-1]);
diff --git a/tests/value/machdep.c b/tests/value/machdep.c
index b901879416538caefa4fafda266ad349c17d7790..8ecb138796265dbe46502f82fcfe314a17bc60d7 100644
--- a/tests/value/machdep.c
+++ b/tests/value/machdep.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable -then -machdep x86_64 -then -machdep x86_16
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_OPTIONS@ -cpp-extra-args="-DPTEST" -journal-disable -then -machdep x86_64 -then -machdep x86_16
*/
#ifndef PTEST
diff --git a/tests/value/nested_struct_init.i b/tests/value/nested_struct_init.i
index f73a3e08021154c466c6ed2c8201e05a41043ace..faf31f6916c2c06bd1d57057a188cbb33196d7e0 100644
--- a/tests/value/nested_struct_init.i
+++ b/tests/value/nested_struct_init.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals maybe -then -lib-entry -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals yes
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@ -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals maybe -then -lib-entry -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals yes
*/
typedef signed char int8_t;
diff --git a/tests/value/origin.i b/tests/value/origin.i
index e00c59f3ba65d431d9c5512683e561f55d1253a6..3707b6875f27548166bfad15b5714433d886619b 100644
--- a/tests/value/origin.i
+++ b/tests/value/origin.i
@@ -1,7 +1,7 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module from,inout,eva @EVA_CONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-main -main main -journal-disable -then -out -deps
- OPT: -no-autoload-plugins -load-module from,inout,eva @EVA_CONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-origin -main origin -journal-disable -then -out -deps
+ OPT: -no-autoload-plugins -load-module from,inout,eva @EVA_OPTIONS@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-main -main main -journal-disable -then -out -deps
+ OPT: -no-autoload-plugins -load-module from,inout,eva @EVA_OPTIONS@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-origin -main origin -journal-disable -then -out -deps
*/
char f(void);
diff --git a/tests/value/postcond_leaf.c b/tests/value/postcond_leaf.c
index 37b99f53706ca6690608d4df5d780720fb0afa04..4afd027255dea30e2adaac0a1ae6e06c2e61b142 100644
--- a/tests/value/postcond_leaf.c
+++ b/tests/value/postcond_leaf.c
@@ -1,5 +1,5 @@
/* run.config*
-OPT: -no-autoload-plugins @EVA_CONFIG@ -load-module eva,inout,report -eva-no-show-progress -eva -eva-use-spec g1,g2,g3 -then -report
+OPT: -no-autoload-plugins @EVA_OPTIONS@ -load-module eva,inout,report -eva-no-show-progress -eva -eva-use-spec g1,g2,g3 -then -report
*/
/* Test what is printed when Value evaluates a post-condition:
diff --git a/tests/value/precond.c b/tests/value/precond.c
index a8c73729935defb33716cd1688cef3fb929786fa..67792a2fbb847f9ebe92de314f596b9f9d1b8e6b 100644
--- a/tests/value/precond.c
+++ b/tests/value/precond.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva,report -lib-entry -eva @EVA_CONFIG@ -then -report -report-print-properties -then -report-no-specialized
+ OPT: -no-autoload-plugins -load-module from,inout,eva,report -lib-entry -eva @EVA_OPTIONS@ -then -report -report-print-properties -then -report-no-specialized
*/
diff --git a/tests/value/precond2.c b/tests/value/precond2.c
index be7006c890e03461fa2cc4e79f8cf0d8096d4125..8934d1a847bc9d6ae83471d08e664e65778a41fd 100644
--- a/tests/value/precond2.c
+++ b/tests/value/precond2.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -rte -then -eva @EVA_CONFIG@ -then -report -report-print-properties
- OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -eva @EVA_CONFIG@ -then -rte -then -report -report-print-properties
+ OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -rte -then -eva @EVA_OPTIONS@ -then -report -report-print-properties
+ OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -eva @EVA_OPTIONS@ -then -rte -then -report -report-print-properties
*/
// Fuse with precond.c when bts #1208 is solved
diff --git a/tests/value/protomain.i b/tests/value/protomain.i
index ff7e47cb0b4932e85d8ffb3a341b0e4f19e3c604..3f06d26dbf7d564a072b79504535d29212b31fc0 100644
--- a/tests/value/protomain.i
+++ b/tests/value/protomain.i
@@ -1,4 +1,4 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_OPTIONS@
*/
int main(int c, char **);
diff --git a/tests/value/recol.c b/tests/value/recol.c
index 46f6de92f5ab375b405205aee08f18c3c344ddcf..e9ac0d03dd0119a3a82f860d223a062a36b1a5bd 100644
--- a/tests/value/recol.c
+++ b/tests/value/recol.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -eva-slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -no-warn-signed-overflow
- OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -eva-slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -machdep ppc_32 -no-warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_OPTIONS@ -eva-slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -no-warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_OPTIONS@ -eva-slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -machdep ppc_32 -no-warn-signed-overflow
*/
#ifndef PTEST
diff --git a/tests/value/recursion.i b/tests/value/recursion.i
index 2b916a17354f17b3e39f216477a7343128c08a36..bf8f1093afad7d590cc1163b08ae9a415cb66221 100644
--- a/tests/value/recursion.i
+++ b/tests/value/recursion.i
@@ -1,6 +1,6 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_CONFIG@ -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_CONFIG@ -eva-ignore-recursive-calls -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_OPTIONS@ -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_OPTIONS@ -eva-ignore-recursive-calls -journal-disable
*/
int G;
diff --git a/tests/value/recursion2.i b/tests/value/recursion2.i
index ec3ea022c9c7e35712cf0f8b466c78c91b7ceace..95c7ec22f964de449e6c15566990ce9e343f9ca7 100644
--- a/tests/value/recursion2.i
+++ b/tests/value/recursion2.i
@@ -1,5 +1,5 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -journal-disable -then -input -out -inout
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_OPTIONS@ -journal-disable -then -input -out -inout
*/
int x, y;
diff --git a/tests/value/redundant_alarms.c b/tests/value/redundant_alarms.c
index 56c24a7649e668e6df92198c864a16a02b0acee2..4231c5c8984eb4f9e4e681c5ea826100abfb16ba 100644
--- a/tests/value/redundant_alarms.c
+++ b/tests/value/redundant_alarms.c
@@ -1,6 +1,6 @@
/* run.config*
- PLUGIN: @EVA_PLUGINS@ slicing sparecode
- OPT: @EVA_CONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -eva-remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
+ PLUGIN: @EVA_CONFIG@ slicing sparecode
+ OPT: @EVA_OPTIONS@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -eva-remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
**/
volatile int v;
diff --git a/tests/value/replace_by_show_each.c b/tests/value/replace_by_show_each.c
index 51592b67f44fd1c183ee2478a67dc16468c4ed9f..5868e433a3665512cefeaad3726605593781202e 100644
--- a/tests/value/replace_by_show_each.c
+++ b/tests/value/replace_by_show_each.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -inout -calldeps
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_OPTIONS@ -inout -calldeps
*/
#define show_each_1 Frama_C_show_each_1
diff --git a/tests/value/sign_of_bitfiled_int.c b/tests/value/sign_of_bitfiled_int.c
index b69aa28c06baafceb1534387dc5b661cbbb20ab1..8af3975b7223773c3be3af35429fa1230d6112d9 100644
--- a/tests/value/sign_of_bitfiled_int.c
+++ b/tests/value/sign_of_bitfiled_int.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -machdep ppc_32 -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_OPTIONS@ -cpp-extra-args="-DPTEST" -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -machdep ppc_32 -eva @EVA_OPTIONS@ -cpp-extra-args="-DPTEST" -journal-disable
*/
diff --git a/tests/value/simplify_cfg.i b/tests/value/simplify_cfg.i
index 5c1b0f1d7193e23bfa1bcbc04740b3aacbd5b681..1e1d7911de7477f96a5a6b7cd846831153a33475 100644
--- a/tests/value/simplify_cfg.i
+++ b/tests/value/simplify_cfg.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -keep-switch -eva @EVA_CONFIG@ -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -eva @EVA_CONFIG@ -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -keep-switch -eva @EVA_OPTIONS@ -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -eva @EVA_OPTIONS@ -journal-disable
*/
int main(int x, int y) {
diff --git a/tests/value/ulongvslonglong.i b/tests/value/ulongvslonglong.i
index c945f20f8813505c233ddf76b4df42533726d3bc..5613d6f0a7e4145d84530abd0f2c04093afc9f99 100644
--- a/tests/value/ulongvslonglong.i
+++ b/tests/value/ulongvslonglong.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -journal-disable -machdep x86_64
- OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_OPTIONS@ -journal-disable -machdep x86_64
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_OPTIONS@ -journal-disable
*/
int x;
diff --git a/tests/value/uninit_callstack.i b/tests/value/uninit_callstack.i
index 6adb7e5120047524db8d21d776a7d7f5d76c9abc..49bb109338ac7c4b5933d939af0534d34175a2ba 100644
--- a/tests/value/uninit_callstack.i
+++ b/tests/value/uninit_callstack.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -eva-no-show-progress -eva-print-callstacks -journal-disable -eva-no-results
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_OPTIONS@ -eva-no-show-progress -eva-print-callstacks -journal-disable -eva-no-results
*/
int *p, x;
diff --git a/tests/value/unknown_sizeof.i b/tests/value/unknown_sizeof.i
index f3a1c3c0c65e3ed31968b58d4531746eba71b228..494dacc33fe3bd5d25090ce97b173c2c0232526e 100644
--- a/tests/value/unknown_sizeof.i
+++ b/tests/value/unknown_sizeof.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -main main1
- OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -main main2
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_OPTIONS@ -main main1
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_OPTIONS@ -main main2
*/
struct s;
diff --git a/tests/value/use_spec.i b/tests/value/use_spec.i
index b22673b3052ae0dc65f6d85e38de74b386760165..df0b292bc31793f47aa5755374ab5947d6497132 100644
--- a/tests/value/use_spec.i
+++ b/tests/value/use_spec.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps -show-indirect-deps
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_OPTIONS@ -inout -calldeps
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_OPTIONS@ -inout -calldeps -show-indirect-deps
*/
diff --git a/tests/value/volatile2.i b/tests/value/volatile2.i
index f1088a88553a2248945e46d4bbb132348729c74f..2829b6cfb49bf264c649606a82fbeb848a1a57c0 100644
--- a/tests/value/volatile2.i
+++ b/tests/value/volatile2.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -print -eva @EVA_CONFIG@ -machdep x86_16
+ OPT: -no-autoload-plugins -load-module from,inout,eva -print -eva @EVA_OPTIONS@ -machdep x86_16
*/
diff --git a/tests/value/widen_overflow.i b/tests/value/widen_overflow.i
index 9bf6480e8085454da2b1e8bacec7f77ba184285a..a184031e23d2989100b77bad22d3333e42bdd2bb 100644
--- a/tests/value/widen_overflow.i
+++ b/tests/value/widen_overflow.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_OPTIONS@
*/
int main() {