From dc7fd4cfa5bec4a8dbd51483cd99ad2416d1c92d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 4 Apr 2019 10:11:18 +0200
Subject: [PATCH] [tests] Renames the macro VALUECONFIG into EVA_CONFIG.
---
src/plugins/value/gen_test_config.sh | 4 ++--
tests/builtins/from_result.c | 2 +-
tests/builtins/malloc-deps.i | 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 | 4 ++--
tests/builtins/test_config_apron | 4 ++--
tests/builtins/test_config_bitwise | 4 ++--
tests/builtins/test_config_equalities | 4 ++--
tests/builtins/test_config_gauges | 4 ++--
tests/builtins/test_config_symblocs | 4 ++--
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 | 8 ++++----
tests/float/precise_cos_sin.c | 2 +-
tests/float/round10d.i | 2 +-
tests/float/some.c | 4 ++--
tests/float/special_floats.i | 2 +-
tests/libc/fc_libc.c | 2 +-
tests/test_config | 4 ++--
tests/test_config_apron | 4 ++--
tests/test_config_bitwise | 4 ++--
tests/test_config_equalities | 4 ++--
tests/test_config_gauges | 4 ++--
tests/test_config_symblocs | 4 ++--
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/from_call.i | 4 ++--
tests/value/ilevel.i | 2 +-
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 | 2 +-
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 +-
81 files changed, 123 insertions(+), 123 deletions(-)
diff --git a/src/plugins/value/gen_test_config.sh b/src/plugins/value/gen_test_config.sh
index 19d3397f175..b1085f08686 100755
--- a/src/plugins/value/gen_test_config.sh
+++ b/src/plugins/value/gen_test_config.sh
@@ -6,8 +6,8 @@
# accordingly. The syntax for the root test_config files is as follows
# (2 lines):
#
-# MACRO: VALUECONFIG <options inherited in all tests>
-# OPT: @VALUECONFIG@ <default options, inherited in tests that use STDOPT>
+# MACRO: EVA_CONFIG <options inherited in all tests>
+# OPT: @EVA_CONFIG@ <default options, inherited in tests that use STDOPT>
# All tested domains
declare -a domains=(
diff --git a/tests/builtins/from_result.c b/tests/builtins/from_result.c
index 4c8c5dc55a2..1076c7ca5bc 100644
--- a/tests/builtins/from_result.c
+++ b/tests/builtins/from_result.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: @VALUECONFIG@ -eva-no-builtins-auto -deps -journal-disable
+ OPT: @EVA_CONFIG@ -eva-no-builtins-auto -deps -journal-disable
*/
#define malloc(n) Frama_C_malloc_fresh(n)
#include "../../share/libc/stdlib.c"
diff --git a/tests/builtins/malloc-deps.i b/tests/builtins/malloc-deps.i
index bd7c49b8400..9c514cf7f03 100644
--- a/tests/builtins/malloc-deps.i
+++ b/tests/builtins/malloc-deps.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
+ OPT: -eva @EVA_CONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
*/
//@ assigns \result \from \nothing;
void *Frama_C_malloc_fresh(unsigned long n);
diff --git a/tests/builtins/malloc-size-zero.c b/tests/builtins/malloc-size-zero.c
index 4b6d9d25485..fdb0c68a789 100644
--- a/tests/builtins/malloc-size-zero.c
+++ b/tests/builtins/malloc-size-zero.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -eva-mlevel 3
- OPT: -eva @VALUECONFIG@ -eva-malloc-functions my_calloc
+ OPT: -eva @EVA_CONFIG@ -eva-mlevel 3
+ OPT: -eva @EVA_CONFIG@ -eva-malloc-functions my_calloc
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index fd550da2c4e..eb00026fa89 100644
--- a/tests/builtins/malloc.c
+++ b/tests/builtins/malloc.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -slevel 10 -eva-mlevel 0
+ OPT: -eva @EVA_CONFIG@ -slevel 10 -eva-mlevel 0
*/
void *Frama_C_malloc_by_stack(unsigned long i);
diff --git a/tests/builtins/malloc_bug_tr.c b/tests/builtins/malloc_bug_tr.c
index dd052d14484..98b3d323d6d 100644
--- a/tests/builtins/malloc_bug_tr.c
+++ b/tests/builtins/malloc_bug_tr.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@
+ OPT: -eva @EVA_CONFIG@
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc_memexec.c b/tests/builtins/malloc_memexec.c
index 004e113f619..463f80de13f 100644
--- a/tests/builtins/malloc_memexec.c
+++ b/tests/builtins/malloc_memexec.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
+ OPT: -eva @EVA_CONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
*/
//@ assigns \result;
diff --git a/tests/builtins/malloc_multiple.c b/tests/builtins/malloc_multiple.c
index 35e3141ad0c..6c807d486a2 100644
--- a/tests/builtins/malloc_multiple.c
+++ b/tests/builtins/malloc_multiple.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -slevel 50 -eva-mlevel 5
+ OPT: -eva @EVA_CONFIG@ -slevel 50 -eva-mlevel 5
*/
#include<stdlib.h>
#define MAX 10
diff --git a/tests/builtins/memcpy_invalid.c b/tests/builtins/memcpy_invalid.c
index 60e26a8463b..cd0a7b35cf7 100644
--- a/tests/builtins/memcpy_invalid.c
+++ b/tests/builtins/memcpy_invalid.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -journal-disable -calldeps
+ OPT: -eva @EVA_CONFIG@ -journal-disable -calldeps
*/
/*@ assigns \result \from min, max;
diff --git a/tests/builtins/test_config b/tests/builtins/test_config
index 08ed11b4566..0958b20e0f2 100644
--- a/tests/builtins/test_config
+++ b/tests/builtins/test_config
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_apron b/tests/builtins/test_config_apron
index 376825b23c6..64f106d0bcf 100644
--- a/tests/builtins/test_config_apron
+++ b/tests/builtins/test_config_apron
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-apron-oct -eva-msg-key experimental-ok
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-apron-oct -eva-msg-key experimental-ok
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_bitwise b/tests/builtins/test_config_bitwise
index a7dce705fef..a084307a988 100644
--- a/tests/builtins/test_config_bitwise
+++ b/tests/builtins/test_config_bitwise
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-bitwise-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-bitwise-domain
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_equalities b/tests/builtins/test_config_equalities
index bdbf2638f30..d10514a2cbe 100644
--- a/tests/builtins/test_config_equalities
+++ b/tests/builtins/test_config_equalities
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-equality-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-equality-domain
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_gauges b/tests/builtins/test_config_gauges
index 49a71af4206..b233bc47b53 100644
--- a/tests/builtins/test_config_gauges
+++ b/tests/builtins/test_config_gauges
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-gauges-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-gauges-domain
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_symblocs b/tests/builtins/test_config_symblocs
index 1e778cb9663..34daa69d9c5 100644
--- a/tests/builtins/test_config_symblocs
+++ b/tests/builtins/test_config_symblocs
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-symbolic-locations-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-symbolic-locations-domain
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/write-const.c b/tests/builtins/write-const.c
index 1dc31cf43b1..89dfcdd91ae 100644
--- a/tests/builtins/write-const.c
+++ b/tests/builtins/write-const.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -journal-disable -eva-builtins-auto -calldeps
+ OPT: -eva @EVA_CONFIG@ -journal-disable -eva-builtins-auto -calldeps
*/
// This test verifies that writing in a memory location that may be const
diff --git a/tests/float/absorb.c b/tests/float/absorb.c
index ca3e781a5f7..a71117b1674 100644
--- a/tests/float/absorb.c
+++ b/tests/float/absorb.c
@@ -1,7 +1,7 @@
/* run.config
COMMENT: run.config is intentionally not-*
EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err FRAMAC_PLUGIN=tests/.empty @frama-c@ -journal-disable -save @PTEST_DIR@/result/absorb.sav @PTEST_FILE@ > @PTEST_DIR@/result/absorb_sav.res 2> @PTEST_DIR@/result/absorb_sav.err
- EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load @PTEST_DIR@/result/absorb.sav -eva @VALUECONFIG@ -journal-disable -float-hex -save @PTEST_DIR@/result/absorb.sav2 > @PTEST_DIR@/result/absorb_sav2.res 2> @PTEST_DIR@/result/absorb_sav2.err
+ EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load @PTEST_DIR@/result/absorb.sav -eva @EVA_CONFIG@ -journal-disable -float-hex -save @PTEST_DIR@/result/absorb.sav2 > @PTEST_DIR@/result/absorb_sav2.res 2> @PTEST_DIR@/result/absorb_sav2.err
OPT: -load @PTEST_DIR@/result/absorb.sav2 -deps -out -input
*/
/* run.config*
diff --git a/tests/float/alarms.i b/tests/float/alarms.i
index 4ab597abb76..8d60a075054 100644
--- a/tests/float/alarms.i
+++ b/tests/float/alarms.i
@@ -1,7 +1,7 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -warn-special-float non-finite
- OPT: -eva @VALUECONFIG@ -warn-special-float nan
- OPT: -eva @VALUECONFIG@ -warn-special-float none
+ OPT: -eva @EVA_CONFIG@ -warn-special-float non-finite
+ OPT: -eva @EVA_CONFIG@ -warn-special-float nan
+ OPT: -eva @EVA_CONFIG@ -warn-special-float none
*/
union { long long l ; float f ; double d ; } u1, u2;
diff --git a/tests/float/builtins.c b/tests/float/builtins.c
index cd0301afa3e..1b2d53069a3 100644
--- a/tests/float/builtins.c
+++ b/tests/float/builtins.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -then -main main_log_exp
+ OPT: -eva @EVA_CONFIG@ -then -main main_log_exp
*/
#include <__fc_builtin.h>
diff --git a/tests/float/cond.c b/tests/float/cond.c
index 10ff9866c04..89cc751c137 100644
--- a/tests/float/cond.c
+++ b/tests/float/cond.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -journal-disable -float-hex
+ OPT: -eva @EVA_CONFIG@ -journal-disable -float-hex
*/
#include "__fc_builtin.h"
diff --git a/tests/float/const.i b/tests/float/const.i
index 24140b0286f..9e47e611f88 100644
--- a/tests/float/const.i
+++ b/tests/float/const.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -float-hex -warn-decimal-float all -journal-disable -then -out -deps
+ OPT: -eva @EVA_CONFIG@ -float-hex -warn-decimal-float all -journal-disable -then -out -deps
*/
typedef double mydouble;
diff --git a/tests/float/extract_bits.i b/tests/float/extract_bits.i
index 1bbd4aa10ec..2f1c3b541cf 100644
--- a/tests/float/extract_bits.i
+++ b/tests/float/extract_bits.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -warn-decimal-float all
- OPT: -eva @VALUECONFIG@ -slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -warn-decimal-float all
+ OPT: -eva @EVA_CONFIG@ -slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -warn-decimal-float all
+ OPT: -eva @EVA_CONFIG@ -slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -warn-decimal-float all
*/
float f = 3.14;
diff --git a/tests/float/init_float.i b/tests/float/init_float.i
index 9812272d6da..83d69d1336e 100644
--- a/tests/float/init_float.i
+++ b/tests/float/init_float.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -journal-disable -float-normal -lib-entry
+ OPT: -eva @EVA_CONFIG@ -journal-disable -float-normal -lib-entry
*/
typedef struct S { float y; } S;
diff --git a/tests/float/nonlin.c b/tests/float/nonlin.c
index 47d55d67984..fce3e9bc0c7 100644
--- a/tests/float/nonlin.c
+++ b/tests/float/nonlin.c
@@ -1,8 +1,8 @@
/* run.config*
- OPT: -eva-msg-key nonlin -slevel 30 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 0
- OPT: -eva-msg-key nonlin -slevel 30 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
- OPT: -eva-msg-key nonlin -slevel 30 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 0
- OPT: -eva-msg-key nonlin -slevel 30 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
+ OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 0
+ OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
+ OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 0
+ OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
*/
#include "__fc_builtin.h"
diff --git a/tests/float/precise_cos_sin.c b/tests/float/precise_cos_sin.c
index d7f40d0632f..19fde982cfb 100644
--- a/tests/float/precise_cos_sin.c
+++ b/tests/float/precise_cos_sin.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -slevel 1000 -journal-disable -float-normal
+ OPT: -eva @EVA_CONFIG@ -slevel 1000 -journal-disable -float-normal
*/
#include <__fc_builtin.h>
diff --git a/tests/float/round10d.i b/tests/float/round10d.i
index b167a89914e..a11f0172aff 100644
--- a/tests/float/round10d.i
+++ b/tests/float/round10d.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -float-normal -journal-disable -no-results
+ OPT: -eva @EVA_CONFIG@ -float-normal -journal-disable -no-results
*/
int main()
diff --git a/tests/float/some.c b/tests/float/some.c
index e8b66bfbd66..d7713ce8d71 100644
--- a/tests/float/some.c
+++ b/tests/float/some.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva-show-slevel 10 -slevel 100 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=double -DN=55" -float-normal -journal-disable -no-results
- OPT: -slevel 100 -eva @VALUECONFIG@ -cpp-extra-args="-DFLOAT=float -DN=26" -float-normal -journal-disable -no-results
+ OPT: -eva-show-slevel 10 -slevel 100 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double -DN=55" -float-normal -journal-disable -no-results
+ OPT: -slevel 100 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float -DN=26" -float-normal -journal-disable -no-results
*/
FLOAT t[N] = { 1. } ;
diff --git a/tests/float/special_floats.i b/tests/float/special_floats.i
index ae1b880cdcd..191afecec7d 100644
--- a/tests/float/special_floats.i
+++ b/tests/float/special_floats.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -warn-special-float none
+ OPT: -eva @EVA_CONFIG@ -warn-special-float none
*/
/* Tests on special float values NaN and infinites. */
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 7f27becef31..7f19d6c406a 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -2,7 +2,7 @@
EXECNOW: make -s @PTEST_DIR@/check_libc_naming_conventions.cmxs
EXECNOW: make -s @PTEST_DIR@/check_const.cmxs
EXECNOW: make -s @PTEST_DIR@/check_parsing_individual_headers.cmxs
- OPT: -load-module @PTEST_DIR@/check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module @PTEST_DIR@/check_const -load-module metrics -eva @VALUECONFIG@ -then -lib-entry -no-print -metrics-no-libc
+ OPT: -load-module @PTEST_DIR@/check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module @PTEST_DIR@/check_const -load-module metrics -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
OPT: -print -print-libc
OPT: -load-module @PTEST_DIR@/check_parsing_individual_headers
CMD: ./tests/libc/check_full_libc.sh
diff --git a/tests/test_config b/tests/test_config
index 2bc92fd4aea..00505a1606c 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_apron b/tests/test_config_apron
index 322d4a9bc6a..dd60e0fbb23 100644
--- a/tests/test_config_apron
+++ b/tests/test_config_apron
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-apron-oct -eva-msg-key experimental-ok
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-apron-oct -eva-msg-key experimental-ok
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise
index 8440d81deff..eee41b0bedc 100644
--- a/tests/test_config_bitwise
+++ b/tests/test_config_bitwise
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-bitwise-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-bitwise-domain
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_equalities b/tests/test_config_equalities
index 18f6799ed4b..962b39797e8 100644
--- a/tests/test_config_equalities
+++ b/tests/test_config_equalities
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-equality-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-equality-domain
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_gauges b/tests/test_config_gauges
index 1840804ec6c..3883074d978 100644
--- a/tests/test_config_gauges
+++ b/tests/test_config_gauges
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-gauges-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-gauges-domain
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index 197dd499d60..34c1fc35dbc 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -1,2 +1,2 @@
-MACRO: VALUECONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-symbolic-locations-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG -eva-show-progress -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-symbolic-locations-domain
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/align_char_array.c b/tests/value/align_char_array.c
index 47c94d0dff2..de692f2f709 100644
--- a/tests/value/align_char_array.c
+++ b/tests/value/align_char_array.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
*/
diff --git a/tests/value/array_initializer.i b/tests/value/array_initializer.i
index 37bce1c2594..04029accd9c 100644
--- a/tests/value/array_initializer.i
+++ b/tests/value/array_initializer.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -then -eva-initialization-padding-globals maybe
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals maybe
*/
int t[5] = { [2] = 3 };
diff --git a/tests/value/array_zero_length.i b/tests/value/array_zero_length.i
index 68f536ad587..f84a4ebf84a 100644
--- a/tests/value/array_zero_length.i
+++ b/tests/value/array_zero_length.i
@@ -1,7 +1,7 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -journal-disable -machdep gcc_x86_32
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -lib-entry -journal-disable -machdep gcc_x86_32
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -lib-entry -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -journal-disable -machdep gcc_x86_32
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable -machdep gcc_x86_32
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable
*/
char T[];
diff --git a/tests/value/base_addr_offset_block_length.i b/tests/value/base_addr_offset_block_length.i
index 6242687662d..4a20889d500 100644
--- a/tests/value/base_addr_offset_block_length.i
+++ b/tests/value/base_addr_offset_block_length.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -context-width 3 -then -slevel 3
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -context-width 3 -then -slevel 3
*/
diff --git a/tests/value/big_lib_entry.i b/tests/value/big_lib_entry.i
index c8f5b717e3d..88a7fbc821a 100644
--- a/tests/value/big_lib_entry.i
+++ b/tests/value/big_lib_entry.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -lib-entry -context-width 4 -eva-initialization-padding-globals no
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -context-width 4 -eva-initialization-padding-globals no
*/
typedef struct {
diff --git a/tests/value/bitfield_longlong.c b/tests/value/bitfield_longlong.c
index f2736abcc60..c2bdb9d6234 100644
--- a/tests/value/bitfield_longlong.c
+++ b/tests/value/bitfield_longlong.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -cpp-extra-args="-Dprintf=Frama_C_show_each" -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-Dprintf=Frama_C_show_each" -journal-disable
*/
struct X50 {
long long int z:50;
diff --git a/tests/value/bts1306.i b/tests/value/bts1306.i
index 9510829da63..f6b51b85784 100644
--- a/tests/value/bts1306.i
+++ b/tests/value/bts1306.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -constfold -slevel 0 -eva @VALUECONFIG@ -print -then -slevel 10 -eva -print
+ OPT: -no-autoload-plugins -load-module from,inout,eva -constfold -slevel 0 -eva @EVA_CONFIG@ -print -then -slevel 10 -eva -print
*/
void g(double x) { double y= x*x; }
diff --git a/tests/value/case_analysis.i b/tests/value/case_analysis.i
index ec27af6dac1..7d9214dd079 100644
--- a/tests/value/case_analysis.i
+++ b/tests/value/case_analysis.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -slevel 30 -journal-disable -float-normal
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -slevel 30 -journal-disable -float-normal
*/
diff --git a/tests/value/cond_integer_cast_of_float.i b/tests/value/cond_integer_cast_of_float.i
index 3d7605a20e5..3a6d8768ec9 100644
--- a/tests/value/cond_integer_cast_of_float.i
+++ b/tests/value/cond_integer_cast_of_float.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @VALUECONFIG@ -no-results -then -float-hex -main mainbis
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -no-results -then -float-hex -main mainbis
*/
typedef double D;
typedef float F;
diff --git a/tests/value/const_typedef.i b/tests/value/const_typedef.i
index 5bbbe2b4ac6..d9f7f3677ca 100644
--- a/tests/value/const_typedef.i
+++ b/tests/value/const_typedef.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -print -then -eva @VALUECONFIG@ -lib-entry -no-print
+ OPT: -no-autoload-plugins -load-module inout,eva -print -then -eva @EVA_CONFIG@ -lib-entry -no-print
*/
typedef int INT[3][3];
diff --git a/tests/value/constarraystructlibentry.i b/tests/value/constarraystructlibentry.i
index 60b87c71f9c..96049bcde85 100644
--- a/tests/value/constarraystructlibentry.i
+++ b/tests/value/constarraystructlibentry.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -lib-entry -eva-initialization-padding-globals yes -then -eva-initialization-padding-globals no
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -eva-initialization-padding-globals yes -then -eva-initialization-padding-globals no
*/
const int t[] = { 1, 2, 3, 4, 5 } ;
diff --git a/tests/value/context_free.i b/tests/value/context_free.i
index 67ecd1b2ea5..19c6fe292ad 100644
--- a/tests/value/context_free.i
+++ b/tests/value/context_free.i
@@ -1,6 +1,6 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -lib-entry -main f -absolute-valid-range 0x200-0x199 -eva-msg-key initial-state -journal-disable
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -main f -absolute-valid-range 0x200-0x199 -eva-msg-key initial-state -journal-disable
*/
diff --git a/tests/value/dead_inout.i b/tests/value/dead_inout.i
index 27070fc23e5..8cf0b0271e6 100644
--- a/tests/value/dead_inout.i
+++ b/tests/value/dead_inout.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -out -input -inout -inout -main main_all
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -out -input -inout -inout -main main_all
*/
// This tests a potential imprecision with the computation of input and outputs if one forgets to test that a statement is dead
diff --git a/tests/value/div.i b/tests/value/div.i
index c19d8f8bfe5..dcea8cf46d4 100644
--- a/tests/value/div.i
+++ b/tests/value/div.i
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-load-module scope -remove-redundant-alarms"
- OPT: -no-autoload-plugins -load-module eva,inout -rte -then -eva @VALUECONFIG@
+ OPT: -no-autoload-plugins -load-module eva,inout -rte -then -eva @EVA_CONFIG@
*/
int X,Y,Z1,Z2,T,U1,U2,V,W1,W2;
int a,b,d1,d2,d0,e;
diff --git a/tests/value/fptr.i b/tests/value/fptr.i
index f9d1014262b..88daeab0630 100644
--- a/tests/value/fptr.i
+++ b/tests/value/fptr.i
@@ -1,7 +1,7 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -journal-disable -then -deps -out
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -main main_uninit -journal-disable -then -deps -out
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -journal-disable -then -deps -out
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main main_uninit -journal-disable -then -deps -out
*/
int R=77; volatile int v; int n;
diff --git a/tests/value/from_call.i b/tests/value/from_call.i
index 54942abc200..c510dd87608 100644
--- a/tests/value/from_call.i
+++ b/tests/value/from_call.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,users,eva -calldeps -eva @VALUECONFIG@ -journal-disable -users -then -input
- OPT: -no-autoload-plugins -load-module from,eva @VALUECONFIG@ -deps -show-indirect-deps -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,users,eva -calldeps -eva @EVA_CONFIG@ -journal-disable -users -then -input
+ OPT: -no-autoload-plugins -load-module from,eva @EVA_CONFIG@ -deps -show-indirect-deps -journal-disable
*/
int a,b,c,d;
int x,y,z,t;
diff --git a/tests/value/ilevel.i b/tests/value/ilevel.i
index 9baf2a45b5a..9cb65bf8796 100644
--- a/tests/value/ilevel.i
+++ b/tests/value/ilevel.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,slicing,sparecode,eva -eva @VALUECONFIG@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48
+ OPT: -no-autoload-plugins -load-module inout,slicing,sparecode,eva -eva @EVA_CONFIG@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48
*/
// Test in particular that ilevel is by-project, even though it is an ocaml ref
volatile int v;
diff --git a/tests/value/incorrect_reduce_expr.i b/tests/value/incorrect_reduce_expr.i
index d82d4c70d9c..0c7f22f6219 100644
--- a/tests/value/incorrect_reduce_expr.i
+++ b/tests/value/incorrect_reduce_expr.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -absolute-valid-range 32-36
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -absolute-valid-range 32-36
*/
char t[5];
diff --git a/tests/value/inout.i b/tests/value/inout.i
index 886eb013822..2e00e3273ac 100644
--- a/tests/value/inout.i
+++ b/tests/value/inout.i
@@ -1,10 +1,10 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -deps -main inout_11_0 -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -deps -main inout_11_3 -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -deps -main never_terminate -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -deps -main may_not_terminate -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -deps -main call_may_not_terminate -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main inout_11_0 -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main inout_11_3 -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main never_terminate -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main may_not_terminate -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main call_may_not_terminate -journal-disable
*/
int Xt, Xs, Xs_I, Ys, Ys_I, Z, I;
diff --git a/tests/value/inout_formals.i b/tests/value/inout_formals.i
index 6bbf367f21f..96883b0436b 100644
--- a/tests/value/inout_formals.i
+++ b/tests/value/inout_formals.i
@@ -1,5 +1,5 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -input-with-formals -inout-with-formals
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -input-with-formals -inout-with-formals
*/
int x, y;
diff --git a/tests/value/inout_proto.i b/tests/value/inout_proto.i
index 2ca51c4b064..977b1591fed 100644
--- a/tests/value/inout_proto.i
+++ b/tests/value/inout_proto.i
@@ -1,5 +1,5 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout @VALUECONFIG@ -inout -input-with-formals -inout-with-formals -main main_main
+ OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -input-with-formals -inout-with-formals -main main_main
*/
typedef unsigned char BYTE;
diff --git a/tests/value/limits.c b/tests/value/limits.c
index 081ea91f82d..965d689d109 100644
--- a/tests/value/limits.c
+++ b/tests/value/limits.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -warn-signed-overflow
*/
#include <limits.h>
diff --git a/tests/value/logic_ptr_cast.i b/tests/value/logic_ptr_cast.i
index 1d85185f09c..6f4c7af2f12 100644
--- a/tests/value/logic_ptr_cast.i
+++ b/tests/value/logic_ptr_cast.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @VALUECONFIG@ -print -journal-disable -no-results
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -print -journal-disable -no-results
*/
int *p;
int t[90];
diff --git a/tests/value/loop_test.i b/tests/value/loop_test.i
index e4658984221..6b1e166139c 100644
--- a/tests/value/loop_test.i
+++ b/tests/value/loop_test.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -main test_onzes -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -main test_cent_onzes -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main test_onzes -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main test_cent_onzes -journal-disable
*/
diff --git a/tests/value/loop_wvar.i b/tests/value/loop_wvar.i
index 2d635fae34d..341e446a0ad 100644
--- a/tests/value/loop_wvar.i
+++ b/tests/value/loop_wvar.i
@@ -1,8 +1,8 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -no-annot -eva @VALUECONFIG@ -then -kernel-warn-key=annot-error=active -annot -eva -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout,eva -kernel-warn-key=annot-error=active -eva @VALUECONFIG@ -main main3 -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @VALUECONFIG@ -main main_err1 -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @VALUECONFIG@ -main main_err2 -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -no-annot -eva @EVA_CONFIG@ -then -kernel-warn-key=annot-error=active -annot -eva -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main3 -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main_err1 -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main_err2 -journal-disable
*/
diff --git a/tests/value/loopinv.c b/tests/value/loopinv.c
index 9da81346949..fbb89b089a4 100644
--- a/tests/value/loopinv.c
+++ b/tests/value/loopinv.c
@@ -1,5 +1,5 @@
/* run.config*
-OPT: @VALUECONFIG@ -no-autoload-plugins -load-module from,inout,eva,report -slevel-function main2:20 -pp-annot -eva -then -report
+OPT: @EVA_CONFIG@ -no-autoload-plugins -load-module from,inout,eva,report -slevel-function main2:20 -pp-annot -eva -then -report
*/
/*@ requires valid: \valid(&t[0..s-1]);
diff --git a/tests/value/machdep.c b/tests/value/machdep.c
index f2164ce8011..b9018794165 100644
--- a/tests/value/machdep.c
+++ b/tests/value/machdep.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -cpp-extra-args="-DPTEST" -journal-disable -then -machdep x86_64 -then -machdep x86_16
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable -then -machdep x86_64 -then -machdep x86_16
*/
#ifndef PTEST
diff --git a/tests/value/nested_struct_init.i b/tests/value/nested_struct_init.i
index 88d885ee6c8..f73a3e08021 100644
--- a/tests/value/nested_struct_init.i
+++ b/tests/value/nested_struct_init.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@ -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals maybe -then -lib-entry -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals yes
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals maybe -then -lib-entry -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals yes
*/
typedef signed char int8_t;
diff --git a/tests/value/origin.i b/tests/value/origin.i
index 4be9a4a8f12..e00c59f3ba6 100644
--- a/tests/value/origin.i
+++ b/tests/value/origin.i
@@ -1,7 +1,7 @@
/* run.config*
GCC:
- OPT: -no-autoload-plugins -load-module from,inout,eva @VALUECONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-main -main main -journal-disable -then -out -deps
- OPT: -no-autoload-plugins -load-module from,inout,eva @VALUECONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-origin -main origin -journal-disable -then -out -deps
+ OPT: -no-autoload-plugins -load-module from,inout,eva @EVA_CONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-main -main main -journal-disable -then -out -deps
+ OPT: -no-autoload-plugins -load-module from,inout,eva @EVA_CONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-origin -main origin -journal-disable -then -out -deps
*/
char f(void);
diff --git a/tests/value/postcond_leaf.c b/tests/value/postcond_leaf.c
index b7171d4133a..37b99f53706 100644
--- a/tests/value/postcond_leaf.c
+++ b/tests/value/postcond_leaf.c
@@ -1,5 +1,5 @@
/* run.config*
-OPT: -no-autoload-plugins @VALUECONFIG@ -load-module eva,inout,report -eva-no-show-progress -eva -eva-use-spec g1,g2,g3 -then -report
+OPT: -no-autoload-plugins @EVA_CONFIG@ -load-module eva,inout,report -eva-no-show-progress -eva -eva-use-spec g1,g2,g3 -then -report
*/
/* Test what is printed when Value evaluates a post-condition:
diff --git a/tests/value/precond.c b/tests/value/precond.c
index 49b21d44e0a..a8c73729935 100644
--- a/tests/value/precond.c
+++ b/tests/value/precond.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva,report -lib-entry -eva @VALUECONFIG@ -then -report -report-print-properties -then -report-no-specialized
+ OPT: -no-autoload-plugins -load-module from,inout,eva,report -lib-entry -eva @EVA_CONFIG@ -then -report -report-print-properties -then -report-no-specialized
*/
diff --git a/tests/value/precond2.c b/tests/value/precond2.c
index 9008ebd7220..be7006c890e 100644
--- a/tests/value/precond2.c
+++ b/tests/value/precond2.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -rte -then -eva @VALUECONFIG@ -then -report -report-print-properties
- OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -eva @VALUECONFIG@ -then -rte -then -report -report-print-properties
+ OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -rte -then -eva @EVA_CONFIG@ -then -report -report-print-properties
+ OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -eva @EVA_CONFIG@ -then -rte -then -report -report-print-properties
*/
// Fuse with precond.c when bts #1208 is solved
diff --git a/tests/value/protomain.i b/tests/value/protomain.i
index 7e8a769384a..ff7e47cb0b4 100644
--- a/tests/value/protomain.i
+++ b/tests/value/protomain.i
@@ -1,4 +1,4 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @VALUECONFIG@
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@
*/
int main(int c, char **);
diff --git a/tests/value/recol.c b/tests/value/recol.c
index a19aaef5016..5d0d3e258ca 100644
--- a/tests/value/recol.c
+++ b/tests/value/recol.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@ -slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -no-warn-signed-overflow
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@ -slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -machdep ppc_32 -no-warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -no-warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -machdep ppc_32 -no-warn-signed-overflow
*/
#ifndef PTEST
diff --git a/tests/value/recursion.i b/tests/value/recursion.i
index a7943ae37f2..2b916a17354 100644
--- a/tests/value/recursion.i
+++ b/tests/value/recursion.i
@@ -1,6 +1,6 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @VALUECONFIG@ -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @VALUECONFIG@ -eva-ignore-recursive-calls -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_CONFIG@ -journal-disable
+ OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_CONFIG@ -eva-ignore-recursive-calls -journal-disable
*/
int G;
diff --git a/tests/value/recursion2.i b/tests/value/recursion2.i
index 7b2a209eda2..ec3ea022c9c 100644
--- a/tests/value/recursion2.i
+++ b/tests/value/recursion2.i
@@ -1,5 +1,5 @@
/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -journal-disable -then -input -out -inout
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -journal-disable -then -input -out -inout
*/
int x, y;
diff --git a/tests/value/redundant_alarms.c b/tests/value/redundant_alarms.c
index 662a3f956db..cd26fec1a2c 100644
--- a/tests/value/redundant_alarms.c
+++ b/tests/value/redundant_alarms.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,scope,slicing,sparecode @VALUECONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
+ OPT: -no-autoload-plugins -load-module inout,scope,slicing,sparecode @EVA_CONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
**/
volatile int v;
diff --git a/tests/value/replace_by_show_each.c b/tests/value/replace_by_show_each.c
index a100f63626e..51592b67f44 100644
--- a/tests/value/replace_by_show_each.c
+++ b/tests/value/replace_by_show_each.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @VALUECONFIG@ -inout -calldeps
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -inout -calldeps
*/
#define show_each_1 Frama_C_show_each_1
diff --git a/tests/value/sign_of_bitfiled_int.c b/tests/value/sign_of_bitfiled_int.c
index efe30e77e34..b69aa28c06b 100644
--- a/tests/value/sign_of_bitfiled_int.c
+++ b/tests/value/sign_of_bitfiled_int.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -machdep ppc_32 -eva @VALUECONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -machdep ppc_32 -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
*/
diff --git a/tests/value/simplify_cfg.i b/tests/value/simplify_cfg.i
index 7b0b780c204..5c1b0f1d719 100644
--- a/tests/value/simplify_cfg.i
+++ b/tests/value/simplify_cfg.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -keep-switch -eva @VALUECONFIG@ -journal-disable
- OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -eva @VALUECONFIG@ -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -keep-switch -eva @EVA_CONFIG@ -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -eva @EVA_CONFIG@ -journal-disable
*/
int main(int x, int y) {
diff --git a/tests/value/ulongvslonglong.i b/tests/value/ulongvslonglong.i
index 54c7fe76c33..c945f20f881 100644
--- a/tests/value/ulongvslonglong.i
+++ b/tests/value/ulongvslonglong.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@ -journal-disable -machdep x86_64
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@ -journal-disable
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -journal-disable -machdep x86_64
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -journal-disable
*/
int x;
diff --git a/tests/value/uninit_callstack.i b/tests/value/uninit_callstack.i
index 86a4a5e5e83..3c1d29d5765 100644
--- a/tests/value/uninit_callstack.i
+++ b/tests/value/uninit_callstack.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @VALUECONFIG@ -eva-no-show-progress -eva-print-callstacks -journal-disable -no-results
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -eva-no-show-progress -eva-print-callstacks -journal-disable -no-results
*/
int *p, x;
diff --git a/tests/value/unknown_sizeof.i b/tests/value/unknown_sizeof.i
index 0d06b705a96..f3a1c3c0c65 100644
--- a/tests/value/unknown_sizeof.i
+++ b/tests/value/unknown_sizeof.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @VALUECONFIG@ -main main1
- OPT: -no-autoload-plugins -load-module eva -eva @VALUECONFIG@ -main main2
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -main main1
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -main main2
*/
struct s;
diff --git a/tests/value/use_spec.i b/tests/value/use_spec.i
index a98064c85ed..b22673b3052 100644
--- a/tests/value/use_spec.i
+++ b/tests/value/use_spec.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @VALUECONFIG@ -inout -calldeps
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @VALUECONFIG@ -inout -calldeps -show-indirect-deps
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps -show-indirect-deps
*/
diff --git a/tests/value/volatile2.i b/tests/value/volatile2.i
index 4a2231374ad..f1088a88553 100644
--- a/tests/value/volatile2.i
+++ b/tests/value/volatile2.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -print -eva @VALUECONFIG@ -machdep x86_16
+ OPT: -no-autoload-plugins -load-module from,inout,eva -print -eva @EVA_CONFIG@ -machdep x86_16
*/
diff --git a/tests/value/widen_overflow.i b/tests/value/widen_overflow.i
index 36960e75ecf..9bf6480e808 100644
--- a/tests/value/widen_overflow.i
+++ b/tests/value/widen_overflow.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @VALUECONFIG@
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@
*/
int main() {
--
GitLab