diff --git a/src/plugins/value/gen_test_config.sh b/src/plugins/value/gen_test_config.sh index 19d3397f175d76a15f46c86fceb781228ebc3223..b1085f0868634319e144ef3549f4518e100638ca 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 4c8c5dc55a2729a3ffdb66688668e56ca3ee395b..1076c7ca5bc3f89a20b05d2ab84271e6dd8226ab 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 bd7c49b8400d7153322e5ebb6ca8c88b16f76122..9c514cf7f03c9190fb7da4c1a475532387800a33 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 4b6d9d25485ae34e6b1ee4f34428569e269764ac..fdb0c68a7895865ceebc92dfed9ccbd6286aeda6 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 fd550da2c4e8e918b56daefc9d2126b8b74126b1..eb00026fa89a438de9352088d7b868c9dadfd809 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 dd052d1448463d4f7e40640326a9baf333d95f99..98b3d323d6dc902fd725994595d35f248190f46b 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 004e113f6197bbcd78285c831de022ed7d246e7f..463f80de13fe6ee4dd098db987ddb42b46659c44 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 35e3141ad0c6badb4b13cf31d8dcf6eadf6d5e79..6c807d486a22e8a16f05c7447c7342a1fe0d8f18 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 60e26a8463bd46ea2c2c3b9a0e111fedab032d6a..cd0a7b35cf7952616fe681aa8959b5bca7feab6e 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 08ed11b4566bf3ec0f00076bee9a279351f7f06e..0958b20e0f2df9755778da617d455c82dcc305d0 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 376825b23c64d0264068c5a6d1e310c6af6a97a0..64f106d0bcfcf55bcf12911b78e37048d5ddc4cc 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 a7dce705feff619ade24257304db07538dbb57bb..a084307a9888678d6a095408724086eddd16543d 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 bdbf2638f30424ef954f1f1d3980ce0080fcda8f..d10514a2cbe43f5ddd94aa9b57ccc254eb75e254 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 49a71af4206b1ca590f23640858ace79657137e2..b233bc47b53b78efa98d658ec88f2fb39a71ebe5 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 1e778cb966369efbec9b7663111bbff65f172626..34daa69d9c5c74f7af6af3d68f2d6326de4d7fd6 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 1dc31cf43b1b253b132f814b145b8b902180c92b..89dfcdd91ae135416df8d7ce0d91a279f41d1235 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 ca3e781a5f7aa215aeca70d81e08c798a4d5cecf..a71117b1674d5f6ba2b6dc97aeacd836c6f275cd 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 4ab597abb76b7592135f018689a32dc1d2686927..8d60a075054d3ed035311ea24ecb62b5f24405c9 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 cd0301afa3e51432ff7ecdfa071d1f8f7c96df56..1b2d53069a31c06abd0b437c3a1b388ed79672e0 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 10ff9866c0400d46f60f48043dbd39e128ab0e40..89cc751c13707df7addc5024e5e5b5aae556091e 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 24140b0286fc7f72aa5d369cc8836dbacac310a5..9e47e611f885b5ad64dbcd15eaeb52c02cde7d27 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 1bbd4aa10ec7f42962669a27176be2df8bc27001..2f1c3b541cf97a2988bad93da7b58dca27a567bf 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 9812272d6da6acebefa819ebe849ad279f9d048f..83d69d1336e42e0cdb64c82e99409c770eba553f 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 47d55d67984bbacb51405f8c641d2c34ce5e6b35..fce3e9bc0c74fc2676ab43a99f858d5f474848bd 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 d7f40d0632ff0fb6bcbd7637885260b7dfdf842c..19fde982cfb2f8367bf5c8b2c201a61dec312b8b 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 b167a89914ec4c85fe3157c8f4ea75c2c44837bb..a11f0172affbc62e6d6e3c270aa8887463b70d62 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 e8b66bfbd66016d1b7d601951a4156400f417ca7..d7713ce8d71d088a7ba48407e83dfc02d1901648 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 ae1b880cdcde14eeca533df5129443f1563eaff7..191afecec7da2c637a90355d92a23dbab8bb23d0 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 7f27becef31786b70e483b2adeda229886900278..7f19d6c406affaba44102e28bf009c3fd50535c2 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 2bc92fd4aeaef3826e3b1bbe196cc94e70e5b7d6..00505a1606c76f45112cfb4051ad44ceeee20b39 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 322d4a9bc6a2ce918eaa1a51add04bfcba58b4da..dd60e0fbb23560f3ce50eb7a6e778d3130c17bba 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 8440d81deff7f93a9ffa247948f1249605339f70..eee41b0bedcf636ed094693962054e8f3ae4c57c 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 18f6799ed4b473b5b0af8d2cbfa888c5c7b327a8..962b39797e8fba2ddc3ba30abd209455b8f19920 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 1840804ec6c6798661e77a1e611104ced98e21f3..3883074d978fa18d856c4fbdedbd292dc35089c4 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 197dd499d60f0879ac68e95ff5fd1d26c6b7dbfc..34c1fc35dbc4c2d8e7647f803bd850098efd056b 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 47c94d0dff2742ca5bc640b82e2f9e392dd4a751..de692f2f709f3533998e31d902afee308ad011df 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 37bce1c25946172877b9df83ffa41418f038821e..04029accd9cbbc52b82684a435bb807b5c29d50a 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 68f536ad5870272b356d4224bfe88b5edefaa2a1..f84a4ebf84a90dfca79e584bfc02975497a704cf 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 6242687662def92ef6f9d0ca4039c63108700f21..4a20889d500dc60519782ff4c15c287bfb360174 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 c8f5b717e3d969ee3c8284d57de157f8b0d333d7..88a7fbc821ae225258a104cb7fd8e57aa28b6445 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 f2736abcc60d1b5cf3ca87090497bb2a8c9ad58e..c2bdb9d6234e025769ac59c269deac5d6f03ec7e 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 9510829da639426ef19637cd1cb1a0e0806099ba..f6b51b857843812b7e4d12234621aee910cce851 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 ec27af6dac1b22bd763942951b3099bc8c3bef52..7d9214dd079a84c2c58e219dd718d5a27b99bb24 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 3d7605a20e54fd48b99cd0886bb99435dd785afa..3a6d8768ec945afce02f2c361459b3d97e9903f7 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 5bbbe2b4ac61247ec64546e56e18a1d24862cc0e..d9f7f3677ca57b9fe40bdc4bfe5b83857a99bc2b 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 60b87c71f9c332c721ce10dc7b097f59eca92fef..96049bcde852de75c8e5efabe6c11fa5d73aca84 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 67ecd1b2ea552d2ceaf2f35225959450711bd72f..19c6fe292ad444d74ab88ef5c0a76fd4c776d76c 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 27070fc23e5626c93bafc1f382a21cef4afc6b0f..8cf0b0271e64bd950206a33e0f67093c1e6bc6c2 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 c19d8f8bfe5f40bda66cc1a68ed9b30e023aa6c9..dcea8cf46d46eb257041662c2645467b92d170aa 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 f9d1014262b879b2ebf54f93c7478f098b4691dd..88daeab0630cbe97a44d8fb52def872d8d5f4bdd 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 54942abc2008129dc2246818b5ad9c6212d8a156..c510dd876084aec37a27264ef03de9b99b79a65f 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 9baf2a45b5aae4d3e1853e904aeda6820f51a583..9cb65bf87964896f8b7a5eb3a95918842bd296e8 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 d82d4c70d9ccde49d1cf918cd7bdbb5e0b5cd5c0..0c7f22f6219efabde4f3dfd99e6eb8e74a44315c 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 886eb013822120623b782ad42c42b08f7af51c88..2e00e3273ace9c6e10ae5ed5e3e74e4578348b9f 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 6bbf367f21f3af08a8ffb5d644d926d0be1e87a8..96883b0436b0ba18a4cf72be2e6d664b4aabe98e 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 2ca51c4b0643dd17e3027ca0fffbe8a3264d53af..977b1591fed06b16f136349a8e77f54120595216 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 081ea91f82d6060b193d7e6c575c6202ebfe3b85..965d689d1099207749cd4e1caab99964a83a2d44 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 1d85185f09c75c053457f590b9698a167880738d..6f4c7af2f12976ac4cab2c017bad0db2d826d135 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 e46589842210d8a573d65205d25fda33eeed05d0..6b1e166139c0aad1abf2f61f4b99233d4639dba5 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 2d635fae34d26333ef5f8193261b68c6135e0fdd..341e446a0ad758d60a6c278b8609dc472a3ccf8b 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 9da813469496b986d7e6d4e5a1134e73011c9f4e..fbb89b089a48133c41a3cfa20648cb9a5b2c633d 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 f2164ce80119b7ca8c4a2872eed611926ea4faa5..b901879416538caefa4fafda266ad349c17d7790 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 88d885ee6c8384db3ef2822c7e90cc2d59de17e2..f73a3e08021154c466c6ed2c8201e05a41043ace 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 4be9a4a8f122b25568557980c4387a7ff6b3b21a..e00c59f3ba65d431d9c5512683e561f55d1253a6 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 b7171d4133a9a6be19c5030b615d8dfacaba0600..37b99f53706ca6690608d4df5d780720fb0afa04 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 49b21d44e0af2c74f8b6561ba9145ca40d1a111b..a8c73729935defb33716cd1688cef3fb929786fa 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 9008ebd722097da73c7115cc4c3da66ed34d7fb8..be7006c890e03461fa2cc4e79f8cf0d8096d4125 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 7e8a769384acc1771b082da46945e5b09fffcd2d..ff7e47cb0b4932e85d8ffb3a341b0e4f19e3c604 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 a19aaef50165bed715cb30007652c3f057388f80..5d0d3e258cafc1c7999e035c68337ba922a2b1db 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 a7943ae37f25a02401cc13ed8c93e216c8d37842..2b916a17354f17b3e39f216477a7343128c08a36 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 7b2a209eda2cba2aa4517a3a851906013a2e7a8d..ec3ea022c9c7e35712cf0f8b466c78c91b7ceace 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 662a3f956db495179243bae16f33f6209f9e84b0..cd26fec1a2c7ab4b10c2b944536d16f4ceff23ee 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 a100f63626e5ff157442876b01adf7d1aa3f78a1..51592b67f44fd1c183ee2478a67dc16468c4ed9f 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 efe30e77e34edefd231fa99d35ab8be77de097d4..b69aa28c06baafceb1534387dc5b661cbbb20ab1 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 7b0b780c2043eb2ad142d226220985bf961bb137..5c1b0f1d7193e23bfa1bcbc04740b3aacbd5b681 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 54c7fe76c339eabafd4c4b9e6a9f5ade959cdaa2..c945f20f8813505c233ddf76b4df42533726d3bc 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 86a4a5e5e833ea581e74cea8a9f9fb3461c35500..3c1d29d57655fbf18f9134cfc186dd1b45ace78a 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 0d06b705a96e26caf96d25728508b9c69e1689fd..f3a1c3c0c65e3ed31968b58d4531746eba71b228 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 a98064c85ed784f7ece55286f0d872ab7383b091..b22673b3052ae0dc65f6d85e38de74b386760165 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 4a2231374ad7d6cc069910c8ca30067a88b57490..f1088a88553a2248945e46d4bbb132348729c74f 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 36960e75ecf5e764feac0ea8640e550fac081d7c..9bf6480e8085454da2b1e8bacec7f77ba184285a 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() {