From 6b4525c237f9df8178371e1a017318ffea3c311c Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 15 Oct 2020 08:32:40 +0200
Subject: [PATCH] [Tests] @EVA_CONFIG@ contents the default plugin list for eva
---
tests/builtins/big_local_array.i | 2 +-
tests/builtins/from_result.c | 2 +-
tests/builtins/malloc-deps.c | 2 +-
tests/builtins/malloc-size-zero.c | 4 ++--
tests/builtins/malloc.c | 2 +-
tests/builtins/malloc_bug_tr.c | 2 +-
tests/builtins/malloc_memexec.c | 2 +-
tests/builtins/malloc_multiple.c | 2 +-
tests/builtins/memcpy_invalid.c | 2 +-
tests/builtins/test_config | 3 +--
tests/builtins/write-const.c | 2 +-
tests/float/absorb.c | 2 +-
tests/float/alarms.i | 6 +++---
tests/float/builtins.c | 2 +-
tests/float/cond.c | 2 +-
tests/float/const.i | 2 +-
tests/float/extract_bits.i | 4 ++--
tests/float/init_float.i | 2 +-
tests/float/nonlin.c | 12 ++++++------
tests/float/precise_cos_sin.c | 2 +-
tests/float/round10d.i | 2 +-
tests/float/some.c | 4 ++--
tests/float/special_floats.c | 2 +-
tests/impact/test_config | 2 +-
tests/journal/control.i | 2 +-
tests/journal/control2.c | 2 +-
tests/journal/intra.i | 2 +-
tests/libc/coverage.c | 2 +-
tests/libc/fc_libc.c | 4 ++--
tests/libc/test_config | 2 +-
tests/misc/add_assigns.i | 2 +-
tests/misc/bts0541.c | 2 +-
tests/misc/bts1347.i | 2 +-
tests/misc/issue109.i | 2 +-
tests/misc/log_twice.i | 2 +-
tests/misc/obfuscate.c | 2 +-
tests/misc/widen_hints.c | 8 ++++----
tests/occurrence/test_config | 2 +-
tests/pdg/bts1194.c | 2 +-
tests/pdg/test_config | 2 +-
tests/rte/test_config | 2 +-
tests/rte/value_rte.c | 2 +-
tests/saveload/load_one.i | 2 +-
tests/scope/bts383.c | 2 +-
tests/scope/no-effect.i | 2 +-
tests/scope/scope.c | 6 +++---
tests/scope/zones.c | 2 +-
tests/slicing/test_config | 2 +-
tests/spec/array_typedef.c | 2 +-
tests/spec/assigns_result.i | 2 +-
tests/spec/assigns_void.c | 4 ++--
tests/spec/behavior_assert.c | 6 +++---
tests/spec/default_assigns_bts0966.i | 2 +-
tests/spec/generalized_check.i | 2 +-
tests/spec/logic_def.c | 2 +-
tests/spec/preprocess.c | 2 +-
tests/spec/shifts.c | 4 ++--
tests/spec/statement_behavior.c | 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 +-
tests/test_config | 5 ++---
tests/value/align_char_array.c | 2 +-
tests/value/array_initializer.i | 2 +-
tests/value/array_zero_length.i | 6 +++---
tests/value/base_addr_offset_block_length.i | 2 +-
tests/value/big_lib_entry.i | 2 +-
tests/value/bitfield_longlong.c | 2 +-
tests/value/bts1306.i | 2 +-
tests/value/case_analysis.i | 2 +-
tests/value/cond_integer_cast_of_float.i | 2 +-
tests/value/const_typedef.i | 2 +-
tests/value/constarraystructlibentry.i | 2 +-
tests/value/context_free.i | 2 +-
tests/value/dead_inout.i | 2 +-
tests/value/div.i | 2 +-
tests/value/fptr.i | 4 ++--
tests/value/incorrect_reduce_expr.i | 2 +-
tests/value/inout.i | 10 +++++-----
tests/value/inout_formals.i | 2 +-
tests/value/inout_proto.i | 2 +-
tests/value/limits.c | 2 +-
tests/value/logic_ptr_cast.i | 2 +-
tests/value/loop_test.i | 4 ++--
tests/value/loop_wvar.i | 8 ++++----
tests/value/loopinv.c | 2 +-
tests/value/machdep.c | 2 +-
tests/value/nested_struct_init.i | 2 +-
tests/value/origin.i | 4 ++--
tests/value/postcond_leaf.c | 2 +-
tests/value/precond.c | 2 +-
tests/value/precond2.c | 4 ++--
tests/value/protomain.i | 2 +-
tests/value/recol.c | 4 ++--
tests/value/recursion.i | 4 ++--
tests/value/recursion2.i | 2 +-
tests/value/redundant_alarms.c | 4 ++--
tests/value/replace_by_show_each.c | 2 +-
tests/value/sign_of_bitfiled_int.c | 4 ++--
tests/value/simplify_cfg.i | 4 ++--
tests/value/ulongvslonglong.i | 4 ++--
tests/value/uninit_callstack.i | 2 +-
tests/value/unknown_sizeof.i | 4 ++--
tests/value/use_spec.i | 4 ++--
tests/value/volatile2.i | 2 +-
tests/value/widen_overflow.i | 2 +-
107 files changed, 151 insertions(+), 153 deletions(-)
diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index 0b931e1f1fe..ce4500f78d0 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 e38ba72eb1c..29020e5dbbe 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 1bb43e5021c..29f258d52bb 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 0ff4c5e749f..21cb95cfe5c 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 989d36b9086..ad4bffd113a 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 98b3d323d6d..c933ffe4af5 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 cac60b4be31..e02637be2be 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 81e2a9cc9f7..337e6b4abfd 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 cd0a7b35cf7..57efefd93f3 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 345f347fd40..05cba93b48e 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 89dfcdd91ae..598d93847eb 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 7a9e3cab596..da1ee88e690 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 8d60a075054..64f4fc79653 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 1b2d53069a3..102f1eff068 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 89cc751c137..3d70579b34f 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 9e47e611f88..207da778ec0 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 08372744719..552bd39549d 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 83d69d1336e..cce205f0527 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 d210fe4a315..e18380a814d 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 f6e6f36e907..271d091d6ba 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 1d6ebe39de5..ba93da532bf 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 8eb3f38ea73..70b34621e96 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 1e07cd3a6ba..67bd40b60be 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 39d00a53e25..c0e7feda3b5 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 0830044b07e..0166aadcd1e 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 f5c82393b8e..c4676ac29be 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 9d3006bde7e..1f063870bdd 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 e11d52b0330..0a63b6c3c76 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 3279d4aa85c..116627e8711 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 cf5c5bb1835..fca40f27463 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 13b86591a9b..e520ee7eb44 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 6bbabaaa30c..213d4e2cd99 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 2df285ccb7d..8313408099a 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 790aa603d9d..1f23c8fe05c 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 dc2306c1c6e..e97f81ad879 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 d28ccfb42f9..3efb19fac6f 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 e4f063807c1..1ececc21c84 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 029a71e6518..f68b112eccd 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 aaa06aacad1..3a8043fdba9 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 78c7757cadf..42a9ea00fb2 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 60080e46918..d265e69bf9f 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 186136b4a70..d614f1cd9aa 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 de48930209e..27120f1a347 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 b2b410d23c7..253a960f6db 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 7b75f9e1d9f..011a3fe5dad 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 a8902199641..8a7d1df5d6f 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 80fc7e30553..7b3d2161b05 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 2a8603f22a8..fff12f16b67 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 a8273f59814..7882dfda139 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 bfde0dde8bf..134947f6cd5 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 a93209867cb..ba4f8a4ac52 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 e130481efd9..30c50494257 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 0bffe80560e..c473d0d55d8 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 0068ae1099a..23ab2c81449 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 8448756e44a..f309563f6bf 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 f0fffe87941..d22f2b661df 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 af132b55019..96e4eb6e892 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 02551271d9e..2e462bd59fd 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 2f475d79ae7..be3439277c2 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 447af8e54b9..43e6f42f933 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 66da8b7cf48..ba204116669 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 38d55c380b6..a1cfdabf081 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 fecc43ece34..5a534c7ec2d 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 de692f2f709..98d2a1d84b5 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 04029accd9c..9ba8114198b 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 f84a4ebf84a..a57db72764c 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 b3aad4d14b7..df95d296e8a 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 0c2770eab0f..6118abf10ce 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 c2bdb9d6234..1f486c7ab6d 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 81f9cc8f329..8ce8ae82294 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 40be501257b..ec832a708da 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 9d1350ea671..00f6714bff5 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 d9f7f3677ca..a6432e9474a 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 96049bcde85..b311d4d4c85 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 19c6fe292ad..581cf60d621 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 8cf0b0271e6..8385ed56381 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 3ac38b6068d..bbbc25443de 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 88daeab0630..d09fb01b4a8 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 0c7f22f6219..91a2bad26a6 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 2e00e3273ac..b3fdc348ff3 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 96883b0436b..bed7b5a38bd 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 977b1591fed..7a0e12c1124 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 965d689d109..d528d6ac4e7 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 64eb43489d6..1d4a9e44fa0 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 6b1e166139c..9037943fb0e 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 341e446a0ad..d07c4120598 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 26f3a1e37b2..3e1e308fb65 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 b9018794165..8ecb1387962 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 f73a3e08021..faf31f6916c 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 e00c59f3ba6..3707b6875f2 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 37b99f53706..4afd027255d 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 a8c73729935..67792a2fbb8 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 be7006c890e..8934d1a847b 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 ff7e47cb0b4..3f06d26dbf7 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 46f6de92f5a..e9ac0d03dd0 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 2b916a17354..bf8f1093afa 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 ec3ea022c9c..95c7ec22f96 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 56c24a7649e..4231c5c8984 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 51592b67f44..5868e433a36 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 b69aa28c06b..8af3975b722 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 5c1b0f1d719..1e1d7911de7 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 c945f20f881..5613d6f0a7e 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 6adb7e51200..49bb109338a 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 f3a1c3c0c65..494dacc33fe 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 b22673b3052..df0b292bc31 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 f1088a88553..2829b6cfb49 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 9bf6480e808..a184031e23d 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() {
--
GitLab