diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index ce4500f78d0b4c0a6747ae45e1762a34ad5e0eae..0b931e1f1fe9931cbf0106a9d8f20d62e8f83c22 100644
--- a/tests/builtins/big_local_array.i
+++ b/tests/builtins/big_local_array.i
@@ -1,5 +1,5 @@
/* run.config*
- PLUGIN: report @EVA_CONFIG@
+ PLUGIN: report @EVA_PLUGINS@
CMXS: big_local_array_script
OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report
OPT: @EVA_OPTIONS@ -load-module %{dep:big_local_array_script.cmxs} -then-on prj -print -report
diff --git a/tests/builtins/test_config b/tests/builtins/test_config
index 05cba93b48eb81c1f37543a85d8dd45f9d70db8d..6d3bfef239211cad7bf4c69404e1f56dd58d6442 100644
--- a/tests/builtins/test_config
+++ b/tests/builtins/test_config
@@ -1,2 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-OPT: -eva @EVA_OPTIONS@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_apron b/tests/builtins/test_config_apron
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_apron
+++ b/tests/builtins/test_config_apron
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_bitwise b/tests/builtins/test_config_bitwise
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_bitwise
+++ b/tests/builtins/test_config_bitwise
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_equalities b/tests/builtins/test_config_equalities
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_equalities
+++ b/tests/builtins/test_config_equalities
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_gauges b/tests/builtins/test_config_gauges
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_gauges
+++ b/tests/builtins/test_config_gauges
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_octagons b/tests/builtins/test_config_octagons
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_octagons
+++ b/tests/builtins/test_config_octagons
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/builtins/test_config_symblocs b/tests/builtins/test_config_symblocs
index e5aae7331927957a07fa55967355b78ed147f1b5..365fdc8d48cbda0c83335a388b0cf9b0d7ceb848 100644
--- a/tests/builtins/test_config_symblocs
+++ b/tests/builtins/test_config_symblocs
@@ -1,3 +1,3 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/cil/mkBinOp.i b/tests/cil/mkBinOp.i
index 9ce55c13e65fae033d97acda1d98088064f30f84..4cd4dae871825623cf523d43735f2ef9bb04ecdf 100644
--- a/tests/cil/mkBinOp.i
+++ b/tests/cil/mkBinOp.i
@@ -1,6 +1,6 @@
/* run.config
MODULE: @PTEST_NAME@
-STDOPT: +"-constfold"
+STDOPT: +"-machdep x86_32 -constfold"
*/
int main(void) {
diff --git a/tests/cil/test_config b/tests/cil/test_config
index ac06bd8d77282c88dbff96fb360889fd14a141bb..3ef8de699a5ff9c1f4ff345e0da4715f09fd6f5b 100644
--- a/tests/cil/test_config
+++ b/tests/cil/test_config
@@ -1,6 +1,6 @@
COMMENT: by default, no analysis is performed (since the PLUGIN directive
COMMENT: is empty).
-COMMENT: to perform value analyses, the macro @EVA_CONFIG@ (resp. @EVA_OPTIONS@)
+COMMENT: to perform value analyses, the macro @EVA_PLUGINS@ (resp. @EVA_OPTIONS@)
COMMENT: can be used into PLUGIN (resp. OPT) directives of specific test files.
COMMENT: no changes of the @DEFAULT_OPTIONS@.
diff --git a/tests/constant_propagation/test_config b/tests/constant_propagation/test_config
index 9b002f56c8cb387e974dcf17de3307c92edaf620..f9f75f643906372c3a5863294c1aef9b95c24d6d 100644
--- a/tests/constant_propagation/test_config
+++ b/tests/constant_propagation/test_config
@@ -1,2 +1,2 @@
-PLUGIN: constant_propagation @PLUGIN@
-OPT: -journal-disable @EVA_OPTIONS@ -scf
+PLUGIN: constant_propagation @PLUGIN@
+OPT: -journal-disable -scf @EVA_OPTIONS@ -machdep x86_32
diff --git a/tests/float/sqrt.c b/tests/float/sqrt.c
index da6743b0866b14d00ea51c2886806bc546008c96..f1cfd10a543687b29631da0c807f25a69fe4223b 100644
--- a/tests/float/sqrt.c
+++ b/tests/float/sqrt.c
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-eva-slevel 10 -big-ints-hex 257"
- STDOPT: #"-eva-slevel 10 -big-ints-hex 257 -machdep ppc_32"
+ STDOPT: #"-eva-slevel 10 -big-ints-hex 257" +"-machdep ppc_32"
*/
#include <math.h>
diff --git a/tests/impact/test_config b/tests/impact/test_config
index c0e7feda3b59d228d66ade073068f424bd328b86..39d00a53e2544038b045de3df9691cb4b61e5f6d 100644
--- a/tests/impact/test_config
+++ b/tests/impact/test_config
@@ -1,2 +1,2 @@
-PLUGIN: impact @EVA_CONFIG@
+PLUGIN: impact @EVA_PLUGINS@
OPT: -journal-disable -impact-print @EVA_OPTIONS@
diff --git a/tests/journal/control2.c b/tests/journal/control2.c
index 2ef7bce9a8c1d9f5e0a1614ea2710190f3c52c5f..82bee121d2731faa4db2bf0eb0225860699edfa4 100644
--- a/tests/journal/control2.c
+++ b/tests/journal/control2.c
@@ -2,7 +2,7 @@
CMXS: control_journal_next2 control_journal2
EXECNOW: BIN control_journal2.ml @frama-c@ -journal-enable -eva -deps -out -main f -journal-name control_journal2.ml > /dev/null 2> /dev/null
EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml @frama-c@ -journal-enable -load-module %{dep:control_journal2.cmxs} -lib-entry -journal-name control_journal_next2.ml > control2_sav.res 2> control2_sav.err
- PLUGIN: callgraph @EVA_CONFIG@
+ PLUGIN: callgraph @EVA_PLUGINS@
OPT: -load-module %{dep:control_journal_next2.cmxs}
*/
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 11a12368cefe9a2a6f78da8fcb1203d9c1d6b71a..b06e6bb6884d605d18172141657fcbf0cb14e04c 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: sparecode @EVA_CONFIG@
+ PLUGIN: sparecode @EVA_PLUGINS@
CMXS: @PTEST_NAME@ intra_journal
EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module %{dep:@PTEST_NAME@.cmxs} -journal-enable -journal-name intra_journal.ml > /dev/null 2> /dev/null
CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs} @OPTIONS@
diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index 0a63b6c3c76a58c550554e41fb1e32a460444168..e11d52b0330129622247b44d9725dc2288d52ec5 100644
--- a/tests/libc/coverage.c
+++ b/tests/libc/coverage.c
@@ -1,5 +1,5 @@
/* run.config*
- PLUGIN: metrics @EVA_CONFIG@
+ PLUGIN: metrics @EVA_PLUGINS@
OPT: -eva-no-builtins-auto @EVA_OPTIONS@ %{read:../../syntax/framac_share_path}/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
*/
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 116627e871111c0fba047d5c60b6ee16e1812273..cf60494482ace1fc64556e8b763f568be70b237c 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -4,9 +4,9 @@
CMXS: check_parsing_individual_headers
CMXS: check_libc_anonymous_tags
CMXS: check_compliance
- PLUGIN: metrics @EVA_CONFIG@
+ PLUGIN: metrics @EVA_PLUGINS@
OPT: -load-module %{dep:check_libc_naming_conventions.cmxs} -print -cpp-extra-args='-nostdinc' -metrics -metrics-libc -load-module %{dep:check_const.cmxs} -eva @EVA_OPTIONS@ -then -lib-entry -no-print -metrics-no-libc
- OPT: -print -print-libc
+ OPT: -print -print-libc -machdep x86_32
OPT: -load-module %{dep:check_parsing_individual_headers.cmxs}
OPT: -load-module %{dep:check_libc_anonymous_tags.cmxs}
OPT: -load-module %{dep:check_compliance.cmxs} -kernel-msg-key printer:attrs
diff --git a/tests/libc/limits_h.c b/tests/libc/limits_h.c
index 8b124df5a62f28a4e70c99720e8db71c00323347..2c663b2c5645c1ac80856c0c08a53b438939debf 100644
--- a/tests/libc/limits_h.c
+++ b/tests/libc/limits_h.c
@@ -1,12 +1,12 @@
/*run.config
- STDOPT: #"-machdep x86_16"
- STDOPT: #"-machdep x86_32"
- STDOPT: #"-machdep x86_64"
- STDOPT: #"-machdep gcc_x86_16"
- STDOPT: #"-machdep gcc_x86_32"
- STDOPT: #"-machdep gcc_x86_64"
- STDOPT: #"-machdep ppc_32"
- STDOPT: #"-machdep msvc_x86_64"
+ STDOPT: +"-machdep x86_16"
+ STDOPT: +"-machdep x86_32"
+ STDOPT: +"-machdep x86_64"
+ STDOPT: +"-machdep gcc_x86_16"
+ STDOPT: +"-machdep gcc_x86_32"
+ STDOPT: +"-machdep gcc_x86_64"
+ STDOPT: +"-machdep ppc_32"
+ STDOPT: +"-machdep msvc_x86_64"
*/
#include <sys/types.h>
#include <stdint.h>
diff --git a/tests/libc/more_gcc_builtins.c b/tests/libc/more_gcc_builtins.c
index d3d023ac786338c8701dd77e2a3baaefbc959b03..614aae666d6e492da1fd8807c239cfe0b305cff8 100644
--- a/tests/libc/more_gcc_builtins.c
+++ b/tests/libc/more_gcc_builtins.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-machdep gcc_x86_32"
+ STDOPT: +"-machdep gcc_x86_32"
*/
volatile int v;
diff --git a/tests/libc/stdlib_h.c b/tests/libc/stdlib_h.c
index ea1b69046d2c3e6452c948df14cccd81439d8ac2..39d9378e90ec0d16f5fdf8ec1b207681e922517c 100644
--- a/tests/libc/stdlib_h.c
+++ b/tests/libc/stdlib_h.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-machdep msvc_x86_64"
+ STDOPT: +"-machdep msvc_x86_64"
*/
// Note: machdep MSVC is used to avoid warnings due to
// "non implemented long double" when testing strtold.
diff --git a/tests/libc/test_config b/tests/libc/test_config
index 237f9df534a80de16aa7bb575c3d9dfcdaf5b2ae..25dfffeef8ee56207ce830aa7482d9424bdeef1b 100644
--- a/tests/libc/test_config
+++ b/tests/libc/test_config
@@ -1 +1 @@
-OPT: -journal-disable -eva @EVA_OPTIONS@ -cpp-extra-args='-nostdinc -Ishare/libc'
+OPT: -eva @EVA_CONFIG@ -cpp-extra-args='-nostdinc -Ishare/libc'
diff --git a/tests/misc/add_assigns.i b/tests/misc/add_assigns.i
index d829e673c473522ddf163c0e551ae2fb3db34a6f..62ee66d75b7c644b67c4f2346e2dad52ee7bd586 100644
--- a/tests/misc/add_assigns.i
+++ b/tests/misc/add_assigns.i
@@ -1,5 +1,5 @@
/* run.config
-PLUGIN: report @EVA_CONFIG@
+PLUGIN: report @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT: -then -report -then -print
*/
diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i
index dab9a7d22dbdbf5bcaacf03e30a4d076b0de65ec..d94078d86dbe4795c2ce5c26396a1f6bd8d802f2 100644
--- a/tests/misc/bts1347.i
+++ b/tests/misc/bts1347.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: report @EVA_CONFIG@
+ PLUGIN: report @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT: @EVA_OPTIONS@ -then -report
*/
diff --git a/tests/misc/obfuscate.c b/tests/misc/obfuscate.c
index 3efb19fac6fe64657cd6cc69a64288e7719ac206..d28ccfb42f935fa60a5de15fad7ce6d072e7d254 100644
--- a/tests/misc/obfuscate.c
+++ b/tests/misc/obfuscate.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: obfuscator @EVA_CONFIG@
+ PLUGIN: obfuscator @EVA_PLUGINS@
OPT: -obfuscate
*/
int my_var = 0;
diff --git a/tests/misc/pragma-pack.c b/tests/misc/pragma-pack.c
index 4e930ec2580967f2cb58acd0405099948af054b7..2f1dbe59e2f928babe15cf58b39293f5d1fa3272 100644
--- a/tests/misc/pragma-pack.c
+++ b/tests/misc/pragma-pack.c
@@ -1,8 +1,8 @@
/*run.config
DEPS: pragma-pack-utils.h
- STDOPT: #"-machdep gcc_x86_64 -kernel-msg-key typing:pragma"
- STDOPT: #"-cpp-command=\"gcc -E -C -I. -m32\" -cpp-frama-c-compliant"
- STDOPT: #"-machdep msvc_x86_64"
+ STDOPT: +"-machdep gcc_x86_64 -kernel-msg-key typing:pragma"
+ STDOPT: +"-machdep gcc_x86_32"
+ STDOPT: +"-machdep msvc_x86_64"
*/
#include "pragma-pack-utils.h"
diff --git a/tests/misc/pragma_pack_zero.c b/tests/misc/pragma_pack_zero.c
index 6a89215bebbdb079321c448fe2c89a718a30a57b..22f956bd3c37c453f011aee30726b8f443dfd79e 100644
--- a/tests/misc/pragma_pack_zero.c
+++ b/tests/misc/pragma_pack_zero.c
@@ -1,6 +1,6 @@
/* run.config
- STDOPT: #"-machdep gcc_x86_64"
- STDOPT: #"-machdep msvc_x86_64"
+ STDOPT: +"-machdep gcc_x86_64"
+ STDOPT: +"-machdep msvc_x86_64"
*/
// #pragma pack(0) is not supported by MSVC, but allowed in GCC.
// In MSVC mode, we ignore it.
diff --git a/tests/more_wp/Makefile b/tests/more_wp/Makefile
deleted file mode 100644
index ebedd46d8a26a0c140278f77977f47a25a38ba2c..0000000000000000000000000000000000000000
--- a/tests/more_wp/Makefile
+++ /dev/null
@@ -1,137 +0,0 @@
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2009 #
-# CEA (Commissariat à l'Énergie Atomique) #
-# INRIA (Institut National de Recherche en Informatique et en #
-# Automatique) #
-# #
-# you can redistribute it and/or modify it under the terms of the GNU #
-# Lesser General Public License as published by the Free Software #
-# Foundation, version 2.1. #
-# #
-# It is distributed in the hope that it will be useful, #
-# but WITHOUT ANY WARRANTY; without even the implied warranty of #
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
-# GNU Lesser General Public License for more details. #
-# #
-# See the GNU Lesser General Public License version v2.1 #
-# for more details (enclosed in the file licenses/LGPLv2.1). #
-# #
-##########################################################################
-
-FD=../..
-WD=$(FD)/tests/more_wp
-WHYDIR=$(FD)/why
-
-EXEC=$(FD)/bin/toplevel.opt
-CMD=FRAMAC_SHARE=$(FD)/share WHYLIB=$(WHYDIR)/lib WHYBIN=$(WHYDIR)/bin/why.opt WHYDP=$(WHYDIR)/bin/why-dp.opt $(EXEC) -journal-disable -wp-verbose 1 -wp-no-bot -wp-proof
-#CMD=FRAMAC_SHARE=$(FD)/share $(EXEC) -journal-disable -wp-verbose 1
-
-all : res_0 res_2
-
-.PHONY : all
-
-JD=$(FD)/tests/jessie
-JFILES=$(wildcard $(JD)/*.c)
-
-WP_FILES=$(JFILES:$(JD)/%.c=$(WD)/%.X)
-STATUS=valid invalid unknown timeout failure
-RES_FILES=$(STATUS:%=%.X) failed.X errors.X
-
-LOG_0=$(WP_FILES:%.X=%.0.log)
-ERR_0=$(WP_FILES:%.X=%.0.err)
-RES_0 = $(RES_FILES:%.X=%.0)
-.PRECIOUS : $(LOG_0) $(ERR_0)
-.PHONY : RES_0
-
-LOG_0 : $(LOG_0)
-ERR_0 : $(ERR_0)
-RES_0 : $(RES_0)
-
-LOG_2=$(WP_FILES:%.X=%.2.log)
-ERR_2=$(WP_FILES:%.X=%.2.err)
-RES_2 = $(RES_FILES:%.X=%.2)
-.PRECIOUS : $(LOG_2) $(ERR_2)
-.PHONY : RES_2
-
-LOG_2 : $(LOG_2)
-ERR_2 : $(ERR_2)
-RES_2 : $(RES_2)
-
-LOG_0 ERR_0 LOG_2 ERR_2 :
- # we need to have a way to store the timestamp
- touch $@
-
-$(WD)/%.0.log $(WD)/%.0.err : $(JD)/%.c $(EXEC)
- -$(CMD) -wp-mm 0 $< > $(WD)/$*.0.log 2> $(WD)/$*.0.err
-
-$(WD)/%.2.log $(WD)/%.2.err : $(JD)/%.c $(EXEC) $(WD)/%.2.no
- @echo "Don't run test M2 for $<"
- touch $@
-
-$(WD)/%.2.log $(WD)/%.2.err : $(JD)/%.c $(EXEC)
- -$(CMD) -wp-mm 2 $< > $(WD)/$*.2.log 2> $(WD)/$*.2.err
-
-errors.% : ERR_%
- -grep Fatal $($<) > $@
- -grep Unbound $($<) >> $@
- -grep "Could not run why" $($<) >> $@
- -grep "Could not run why" $(LOG_$*) >> $@
- echo "TOTAL errors = `wc -l $@`" >> $@
-
-failed.% : LOG_%
- -grep Failed $($<) > $@
- echo "TOTAL failed = `wc -l $@`" >> $@
-
-%.0 : $(LOG_0)
- -grep $* $+ | grep "%" | grep -v " 0%" > $@
- echo "TOTAL $* = \
- `gawk 'BEGIN { cpt = 0; } { cpt += $$3; } END { print cpt; }' \
- $@`" >> $@
-
-%.2 : $(LOG_2)
- -grep $* $+ | grep "%" | grep -v " 0%" > $@
- echo "TOTAL $* = \
- `gawk 'BEGIN { cpt = 0; } { cpt += $$3; } END { print cpt; }' \
- $@`" >> $@
-
-res_% : RES_%
- @echo "=== Results for model $* :"
- grep "TOTAL" $($<) > $@
- cat $@
-
-failed.%.m : failed.% Makefile
- cat $< \
- | grep -v " [cfg] switch handling" \
- | grep -v " char constant expr" \
- | grep -v " string constant expr" \
- | grep -v " cast" \
- | grep -v " logic function with labels" \
- | grep -v " predicate with label" \
- | grep -v " fol term range" \
- | grep -v " unsupported C or logic type" \
- > $@
-
-
-# identification of "normal" (or known) failed cases
-f0 : failed.0.m
- -cat $< \
- | grep -v ": indirect assign" \
- | grep -v ": indirect access" \
- | grep -v ": no assigns clause in called function" \
-
-f2 : failed.2.m
- -cat $< \
- | grep -v ": pointer to logic_type not implemented" \
-
-clean :
- rm -f $(LOG_0) $(ERR_0) $(RES_0) LOG_0 ERR_0 RES_0
- rm -f $(LOG_2) $(ERR_2) $(RES_2) LOG_2 ERR_2 RES_2
- rm -f frama_c_journal.ml
- rm -f failed.*.m res_0 res_2
- rm -f gwhy.cache
-
-# .SILENT :
-
diff --git a/tests/more_wp/TODO b/tests/more_wp/TODO
deleted file mode 100644
index c634c171f0f3744784d927ef434377c42599daf1..0000000000000000000000000000000000000000
--- a/tests/more_wp/TODO
+++ /dev/null
@@ -1,31 +0,0 @@
-- traiter les " global invariant".
- exemple : ../jessie/band.c
- ../../init.c
-- gestion des variables globales const ?
- exemple : ../../init2.c
-- 2 alloc donne des pointeurs différents
- exemple : ../../alloc.c
-- ajouter les axiomes dans le fichiers why
- exemple : ../../count_bits.c
-- intervale pour un enum (se ramener à un invariant de type ?)
- exemple : ../../enum.c
-- predicate avec label
- exemple : ../../glob.c
-
-- détection des labels non traités
-
-- étudier les tests :
- ../../weber3.c
- bubblesort.c
- quicksort.c
-
-- pb traduction des définitions de prédicats en M2
- (doit-on faire intervenir la memoire ou non ???)
- exemple : ../../interval_arith.c avec M2
-
-
-DONE :
-- simplification des let et forall
-- behaviors
-- some casts (integer -> integer and real -> real)
-- base_id for local variables
diff --git a/tests/more_wp/bubblesort.c b/tests/more_wp/bubblesort.c
deleted file mode 100644
index 74d383c4e633efc5e3b070e944750fa486887e55..0000000000000000000000000000000000000000
--- a/tests/more_wp/bubblesort.c
+++ /dev/null
@@ -1,100 +0,0 @@
-int a[100];
-
- /*@
- predicate my_sorted_array(int old_a[], integer start_index, integer end_index) =
- \forall integer k1, k2;
- start_index <= k1 <= k2 <= end_index ==> a[k1] <= a[k2];
-*/
-
-
-/*@
- predicate all_smaller_than_the_last (int old_a[], integer start_index, integer end_index) =
- \forall integer k1;
- start_index <= k1 < end_index ==> a[k1] <= a[end_index];
-*/
-
-
-
-//use of swap funktion causes ERROR
-
-/*@
- requires 0 < length;
- requires \valid_range(a, 0, length-1);
- ensures my_sorted_array(a, 0, length-1);
-*/
-void bubble_sort(int* old_a, int length)
-{
-
-
- int auf = 1;
- int ab;
- int fixed_auf = auf;
-
- /*@
- loop invariant fixed_auf == auf;
- loop invariant 0 < auf <= length;
- loop invariant all_smaller_than_the_last(a, 0, auf-1);
- loop invariant my_sorted_array(a, 0, auf-1);
- loop invariant \forall integer k; auf < k < length ==> a[k] == \at(a[k], Pre);
- loop assigns auf, fixed_auf, ab, a[0..auf];
- */
- for (; auf < length; auf++, fixed_auf = auf)
- {
- //@ assert my_sorted_array(a, 0, auf-1); //IMPORTANT
- fixed_auf = auf;
- ab=auf;
- //@ assert my_sorted_array(a, ab, auf);
- /*@
- loop invariant fixed_auf == auf;
- loop invariant 0 <= ab <= auf;
- loop invariant all_smaller_than_the_last(a, 0, auf-1);
- loop invariant my_sorted_array(a, 0, ab-1);
- loop invariant my_sorted_array(a, ab, auf);
-
- loop invariant \forall integer k; auf < k < length ==> a[k] == \at(a[k], Pre);
- loop assigns ab, a[0..auf];
- */
- while (0 < ab && a[ab] < a[ab-1])
- {
- //@ assert my_sorted_array(a, 0, ab-1); //IMPORTANT
- //@ assert my_sorted_array(a, ab, auf); //IMPORTANT
-
-
- //@ assert a[ab] < a[ab-1]; //IMPORTANT
- //@ assert a[ab] <= a[auf];
-
- int temp = a[ab];
- a[ab] = a[ab-1];
- a[ab-1] = temp;
-
-
- //@ assert a[ab-1] <= a[ab]; //IMPORTANT
- // not completely correct (actually <), because only swapped when a[ab] < a[ab-1],
-
-
- //@ assert my_sorted_array(a, ab+1, auf); // OK
-
- //@ assert a[ab] <= a[auf];
- //Problem: should be correct but is not proven
- //Solved: is proven due to predicate "all_smaller_than_the_last"
-
- //@ assert my_sorted_array(a, 0, ab-2); //ok //IMPORTANT
-
- //@ assert ab < auf ==> all_smaller_than_the_last(a, ab, ab+1);
- // NEEDS TO BE PROVEN
-
- //@ assert a[ab] <= a[auf];
- // NEEDS TO BE PROVEN
- //@ assert my_sorted_array(a, ab, auf); // FAILURE
-
- // ==>
- //@ assert my_sorted_array(a, ab-1, auf); //IMPORTANT
-
- ab = ab-1;
- //@ assert my_sorted_array(a, 0, ab-1); //IMPORTANT
- //@ assert my_sorted_array(a, ab, auf); //IMPORTANT
- }
- //@ assert my_sorted_array(a, 0, auf); //IMPORTANT
- }
-}
-
diff --git a/tests/more_wp/quicksort.c b/tests/more_wp/quicksort.c
deleted file mode 100644
index cbb9f0fb0ce49b485ff07b850e25c1b90c3962b1..0000000000000000000000000000000000000000
--- a/tests/more_wp/quicksort.c
+++ /dev/null
@@ -1,130 +0,0 @@
-/* FRAMAC_SHARE=share bin/viewer.opt -pp-annot quicksort.c */
-
-/*external permut_ij : ptr -> ptr -> int -> int -> Prop : Quicksort ;
-external permut : ptr -> ptr -> Prop : Quicksort ;
-external high_bound : ptr -> int -> int -> int -> Prop : Quicksort ;
-external low_bound : ptr -> int -> int -> int -> Prop : Quicksort ;
-*/
-
-#define SIZE 100
-int T[SIZE];
-
-/*@ requires (0 <= i < SIZE) && (0 <= j < SIZE);
- ensures T[i] == \old(T[j]) && T[j] == \old(T[i]);
- assigns T[i], T[j];
- */
-void swap (int i, int j) {
- int v;
- v = T[i];
- T[i] = T[j];
- T[j] = v;
-}
-
-/*@
-requires (0 <= l < i) && (i < SIZE)
- && (\forall int k; l+1 <= k <= i-1 ==> T[k] <= T[l]);
-ensures i-1 <= \result <= i
- && (\forall int k; l <= k <= \result ==> T[k] <= T[\result])
- && (\forall int res; res == \result ==>
- T[l] == \old(T[res]) && T[res] == \old(T[l]))
- && T[\result] <= T[i];
-*/
-int mv_pv (int l, int i) {
- int res;
- if (T[i] < T[l]) {
- swap(l, i);
- res = i;
- }
- else {
- swap(l, i - 1);
- res = i - 1;
- }
- return res;
-}
-
-
-/*
-Pre : (0 <= l < r) && r < length(T);
-Modifies : T;
-Post :
- (l <= result && result <= r) &&
- high_bound (T, l, result, T[result]) &&
- low_bound (T, result, r, T[result]) &&
- permut (T, T@0) &&
- (forall k:int. (k < l \/ k > r) => T[k] = T@0[k]);
-*/
-int partition (int l, int r)
-{
- int pv, i, j, res;
- pv = T[l];
- i = l+1;
- j = r;
-
- while (i < j)
- /*
- Inv: (l+1 <= i <= r) && j <= r && i <= j+1 && permut (T, T@0)
- && high_bound (T, l+1, i-1, pv) && (low_bound (T, j+1, r, pv))
- && (forall k:int. (k <= l \/ k > r) => T[k] = T@0[k]);
- Modifies : i, j, T;
- */
- {
- while (T[i] <= pv && i < j)
- /*
- Inv: l+1 <= i <= r && high_bound (T, l+1, i-1, pv) && i <= j+1;
- Modifies : i;
- */
- { i = i + 1; }
-
- while (T[j] >= pv && i < j)
- /*
- Inv: j <= r && low_bound (T, j+1, r, pv)
- && ~(T[i] <= pv && i < j) && i <= j+1;
- Modifies : j;
- */
- { j = j - 1; }
-
- if (i < j)
- {
- swap( i, j);
- i = i + 1;
- j = j - 1;
- }
- }
-
- res = mv_pv (l, i);
-
- return res;
-}
-
-
-/*
-Pre: 0 <= l && r < length(T);
-Modifies: T;
-
-Post:
- (forall i j:int. l <= i <= j <= r => T[i] <= T[j]) &&
- (forall k:int. (k < l \/ k > r) => T[k] = T@0[k]) &&
- permut (T, T@0) ;
- */
-
-void quick_rec (int l, int r)
-{
- int p;
- if (l < r)
- {
- p = partition(l, r);
- quick_rec(l, p-1);
- quick_rec(p+1, r);
- }
-}
-
-/*
-void sort (int n)
-Pre: n = length (T);
-Modifies: T;
-{
- quick_rec (0, n-1);
-}
-Post : (forall i j:int. (0 <= i <= j < n) => T[i] <= T[j]) &&
- permut (T, T@0) ;
-*/
diff --git a/tests/occurrence/test_config b/tests/occurrence/test_config
index f68b112eccd0e3a541bae9a937c28569b2a732f7..029a71e6518323c3e32e2950e023ee1bf8687253 100644
--- a/tests/occurrence/test_config
+++ b/tests/occurrence/test_config
@@ -1,2 +1,2 @@
-PLUGIN: occurrence @EVA_CONFIG@
+PLUGIN: occurrence @EVA_PLUGINS@
STDOPT: -"-eva" -"-out" -"-input" -"-deps" +"-occurrence-verbose 1"
diff --git a/tests/pdg/bts1194.c b/tests/pdg/bts1194.c
index 3a8043fdba9906c389defb22b841e23d207431b6..aaa06aacad1c5038696f57e95c6f557179be2f34 100644
--- a/tests/pdg/bts1194.c
+++ b/tests/pdg/bts1194.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: slicing @EVA_CONFIG@
+ PLUGIN: slicing @EVA_PLUGINS@
STDOPT: +"-eva -inout -pdg -calldeps -deps -then -slice-return main -then-last -print @EVA_OPTIONS@"
*/
diff --git a/tests/pdg/test_config b/tests/pdg/test_config
index 42a9ea00fb225a1a746d93560735058a8410ad5f..78c7757cadf8d143e6823856234b4ab43b1a3839 100644
--- a/tests/pdg/test_config
+++ b/tests/pdg/test_config
@@ -1,2 +1,2 @@
-PLUGIN: pdg @EVA_CONFIG@
+PLUGIN: pdg @EVA_PLUGINS@
OPT: -journal-disable @EVA_OPTIONS@ -pdg-print -pdg-verbose 2
diff --git a/tests/pretty_printing/test_config b/tests/pretty_printing/test_config
index cb1129105e58806d9244aa0703b4f445ce3b6e71..523c8ad970ed4efa6d6a28a7dad3557b2ad46a8a 100644
--- a/tests/pretty_printing/test_config
+++ b/tests/pretty_printing/test_config
@@ -3,7 +3,7 @@ COMMENT: the default option checks that pretty-printed code can be merged
COMMENT: with the original one.
COMMENT: by default, no analysis is performed (since the PLUGIN directive
COMMENT: is empty).
-COMMENT: to perform value analyses, the macro @EVA_CONFIG@ (resp. @EVA_OPTIONS@)
+COMMENT: to perform value analyses, the macro @EVA_PLUGINS@ (resp. @EVA_OPTIONS@)
COMMENT: can be used into PLUGIN (resp. OPT) directives of specific test files.
PLUGIN:
diff --git a/tests/ptests_config b/tests/ptests_config
index 301ad30532ecec0afd103bcf1c9cf08938324916..581b0bbb0abd5f831643143c3014e33191639a0b 100644
--- a/tests/ptests_config
+++ b/tests/ptests_config
@@ -1,7 +1,6 @@
# todo: adds bugs?
# todo: adds crowbar?
# todo: adds dynamic_plugin? No, will be removed from master branch.
-# todo: adds more_wp? No, will be removed from master branch.
# todo: adds verisec?
DEFAULT_SUITES= builtins callgraph cil constant_propagation dynamic fc_script float idct impact
diff --git a/tests/rte/test_config b/tests/rte/test_config
index d265e69bf9fe0845ca3de4103ff2a4cd25ec1fe6..60080e46918d03b8587ae6b09528301f66b0ae50 100644
--- a/tests/rte/test_config
+++ b/tests/rte/test_config
@@ -1 +1 @@
-PLUGIN: rtegen @EVA_CONFIG@
+PLUGIN: rtegen @EVA_PLUGINS@
diff --git a/tests/rte/value_rte.c b/tests/rte/value_rte.c
index d614f1cd9aaabce832282232cf57092ed74e8b5e..186136b4a704446ee7e2c38e9d059310ada50207 100644
--- a/tests/rte/value_rte.c
+++ b/tests/rte/value_rte.c
@@ -1,5 +1,5 @@
/* run.config
-PLUGIN: report @EVA_CONFIG@
+PLUGIN: report @EVA_PLUGINS@
OPT: -rte -then -eva @EVA_OPTIONS@ -then -report
*/
diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c
index 776352ac0a54fc32edd606bd9407fa8b04bce754..200d545f557c3f08fa5599075baf01efa4eb38a4 100644
--- a/tests/saveload/bool.c
+++ b/tests/saveload/bool.c
@@ -1,5 +1,5 @@
/* run.config
- EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err @frama-c@ -save bool.sav -eva @EVA_OPTIONS@ > bool_sav.res 2> bool_sav.err
+ EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err @frama-c@ -save bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ > bool_sav.res 2> bool_sav.err
STDOPT: +"-load %{dep:bool.sav} -out -input -deps"
STDOPT: +"-load %{dep:bool.sav} -eva @EVA_OPTIONS@"
*/
diff --git a/tests/saveload/load_one.i b/tests/saveload/load_one.i
index a223064c22fb4320836161de1edd167b6b98274f..cb33a395e5a231927cc4b11960a67b54b75337d2 100644
--- a/tests/saveload/load_one.i
+++ b/tests/saveload/load_one.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: sparecode @EVA_CONFIG@
+ PLUGIN: sparecode @EVA_PLUGINS@
MODULE: @PTEST_NAME@
STDOPT:
*/
diff --git a/tests/scope/zones.c b/tests/scope/zones.c
index 7b3d2161b05f23f52f8bf294f528db68c78237d2..80fc7e30553dbf463b58bf27048435c76d607838 100644
--- a/tests/scope/zones.c
+++ b/tests/scope/zones.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@ pdg
+ PLUGIN: @EVA_PLUGINS@ pdg
CMXS: @PTEST_NAME@
OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -eva @EVA_OPTIONS@ -journal-disable
*/
diff --git a/tests/slicing/test_config b/tests/slicing/test_config
index 4ca5fca8bac218ebd7240d0fd78c85478ff9c118..70059f8e01cc1a595bc0763eacdf15f3a4989f50 100644
--- a/tests/slicing/test_config
+++ b/tests/slicing/test_config
@@ -1,2 +1,2 @@
-PLUGIN: slicing @EVA_CONFIG@
-OPT: @EVA_OPTIONS@ -journal-disable
+PLUGIN: slicing @EVA_PLUGINS@
+OPT: @EVA_OPTIONS@ -machdep x86_32
diff --git a/tests/spec/array_typedef.c b/tests/spec/array_typedef.c
index 7882dfda13967c35fcfc11f06c22a791ad95ea42..a8273f598146e1ddb45647df4ec7477d47f347f9 100644
--- a/tests/spec/array_typedef.c
+++ b/tests/spec/array_typedef.c
@@ -1,5 +1,5 @@
/*run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
OPT: -print -eva @EVA_OPTIONS@ -journal-disable
*/
#define IP_FIELD 4
diff --git a/tests/spec/assigns_result.i b/tests/spec/assigns_result.i
index 134947f6cd5b6b73493037c82f51020c507b2caa..bfde0dde8bfeafeac8e63a972479dfcc80b2e97e 100644
--- a/tests/spec/assigns_result.i
+++ b/tests/spec/assigns_result.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-deps @EVA_OPTIONS@"
*/
int X,Y;
diff --git a/tests/spec/assigns_void.c b/tests/spec/assigns_void.c
index ba4f8a4ac52f3f6b16fed4285d3640e3486f783a..6f993130b393da08bec490ea77cb1ef26a967e29 100644
--- a/tests/spec/assigns_void.c
+++ b/tests/spec/assigns_void.c
@@ -1,6 +1,6 @@
/* run.config
OPT: -print -journal-disable -kernel-warn-key=annot-error=active
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_OPTIONS@ -main g -print -no-annot -journal-disable
*/
//@ assigns *x;
diff --git a/tests/spec/behavior_assert.c b/tests/spec/behavior_assert.c
index 30c5049425710c4c550b9119068fb2c46cba5278..2e8732b4b649003ae76f904be3847c7d476966a7 100644
--- a/tests/spec/behavior_assert.c
+++ b/tests/spec/behavior_assert.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_OPTIONS@ -deps -out -input -journal-disable -lib-entry
OPT: -eva @EVA_OPTIONS@ -deps -out -input -journal-disable
*/
diff --git a/tests/spec/default_assigns_bts0966.i b/tests/spec/default_assigns_bts0966.i
index c473d0d55d851272fd54a6f74679b71ce4ae0a47..0bffe80560eef462f8bf954d9093a8b8d854ed30 100644
--- a/tests/spec/default_assigns_bts0966.i
+++ b/tests/spec/default_assigns_bts0966.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
OPT: -eva -print
*/
int auto_states[4] ; // = { 1 , 0 , 0, 0 };
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 23ab2c814494dc31ce1740bae6018d8e7954ca94..9f3a2f6a735feb5c3f5193624453932040b6ec29 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,6 +1,4 @@
/* run.config
-PLUGIN: wp @EVA_CONFIG@
-OPT: -wp -wp-prover qed -wp-msg-key shell
OPT: -eva -eva-use-spec f
OPT: -print
*/
diff --git a/tests/spec/logic_def.c b/tests/spec/logic_def.c
index f309563f6bf1f7fd46e46fb1d3bb0aa4358fb2af..8448756e44a5693e646a07608132edc247187e26 100644
--- a/tests/spec/logic_def.c
+++ b/tests/spec/logic_def.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-eva -eva-verbose 2"
*/
//@ logic integer foo(int x) = x + 2 ;
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
index 33aea489a5e768242a7bccd3063352353e4c370f..f93e7228b403b708b01b4386186ab29d200d1a5a 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -1,24 +1,47 @@
-# frama-c -wp [...]
-[kernel] Parsing generalized_check.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] generalized_check.i:31: Warning:
- Unsupported generalized invariant, use loop invariant instead.
- Ignored invariant
- check invariant \true;
-[wp] Warning: Missing RTE guards
-[wp] generalized_check.i:38: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] 11 goals scheduled
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Failed] Goal typed_f_check_f_valid_ko
-[wp] [Qed] Goal typed_f_check_ensures_f_init_x : Valid
-[wp] [Failed] Goal typed_check_lemma_easy_proof
-[wp] [Qed] Goal typed_loop_loop_assigns : Valid
-[wp] [Failed] Goal typed_loop_check_implied_by_false_invariant
-[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_established
-[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved
-[wp] [Failed] Goal typed_main_call_f_check_requires_f_valid_x
-[wp] [Failed] Goal typed_main_check_main_p_content_ko
-[wp] [Failed] Goal typed_main_check_main_valid_ko
-[wp] Proved goals: 3 / 11
- Qed: 3
+[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva:alarm] tests/spec/generalized_check.i:23: Warning:
+ accessing uninitialized left-value. assert \initialized(&c);
+[eva] using specification for function f
+[eva:alarm] tests/spec/generalized_check.i:24: Warning:
+ function f: precondition 'f_valid_x' got status unknown.
+[eva] tests/spec/generalized_check.i:9: Warning:
+ no \from part for clause 'assigns *x;'
+[eva:alarm] tests/spec/generalized_check.i:25: Warning:
+ check 'main_valid_ko' got status unknown.
+[eva:alarm] tests/spec/generalized_check.i:26: Warning:
+ check 'main_p_content_ko' got status unknown.
+[eva:alarm] tests/spec/generalized_check.i:32: Warning:
+ loop invariant 'false_but_preserved' got status invalid.
+[eva] tests/spec/generalized_check.i:35: starting to merge loop iterations
+[eva:alarm] tests/spec/generalized_check.i:36: Warning:
+ check 'implied_by_false_invariant' got status invalid.
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function loop:
+ j ∈ {10}
+[eva:final-states] Values at end of function main:
+ a ∈ [--..--]
+ p ∈ {{ NULL ; &a }}
+ __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 3 functions analyzed (out of 3): 100% coverage.
+ In these functions, 25 statements reached (out of 28): 89% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 1 warning
+ by the Frama-C kernel: 0 errors 0 warnings
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 access to uninitialized left-values
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 2 unknown 2 invalid 4 total
+ Preconditions 0 valid 1 unknown 0 invalid 1 total
+ 0% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/tests/spec/oracle/generalized_check.1.res.oracle b/tests/spec/oracle/generalized_check.1.res.oracle
index 60b7e824fa4d4724c596df28d617622cbaba7947..7e0503ac2ae81e3733b87703e497dee35f843332 100644
--- a/tests/spec/oracle/generalized_check.1.res.oracle
+++ b/tests/spec/oracle/generalized_check.1.res.oracle
@@ -1,46 +1,51 @@
[kernel] Parsing generalized_check.i (no preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-
-[eva:alarm] generalized_check.i:24: Warning:
- accessing uninitialized left-value. assert \initialized(&c);
-[eva] using specification for function f
-[eva:alarm] generalized_check.i:25: Warning:
- function f: precondition 'f_valid_x' got status unknown.
-[eva] generalized_check.i:10: Warning: no \from part for clause 'assigns *x;'
-[eva:alarm] generalized_check.i:26: Warning:
- check 'main_valid_ko' got status unknown.
-[eva:alarm] generalized_check.i:27: Warning:
- check 'main_p_content_ko' got status unknown.
-[eva:alarm] generalized_check.i:33: Warning:
- loop invariant 'false_but_preserved' got status invalid.
-[eva] generalized_check.i:36: starting to merge loop iterations
-[eva:alarm] generalized_check.i:37: Warning:
- check 'implied_by_false_invariant' got status invalid.
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function loop:
- j ∈ {10}
-[eva:final-states] Values at end of function main:
- a ∈ [--..--]
- p ∈ {{ NULL ; &a }}
- __retres ∈ {0}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 3 functions analyzed (out of 3): 100% coverage.
- In these functions, 25 statements reached (out of 28): 89% coverage.
- ----------------------------------------------------------------------------
- Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 1 warning
- by the Frama-C kernel: 0 errors 0 warnings
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 access to uninitialized left-values
- ----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 0 valid 2 unknown 2 invalid 4 total
- Preconditions 0 valid 1 unknown 0 invalid 1 total
- 0% of the logical properties reached have been proven.
- ----------------------------------------------------------------------------
+/* Generated by Frama-C */
+/*@ check lemma easy_proof: \false;
+ */
+/*@ check requires f_valid_x: \valid(x);
+ check ensures f_init_x: *\old(x) ≡ 0;
+ assigns *x;
+ */
+void f(int *x)
+{
+ /*@ check f_valid_ko: \valid(x); */ ;
+ *x = 0;
+ return;
+}
+
+void loop(void);
+
+int main(void)
+{
+ int __retres;
+ int volatile c;
+ int a = 4;
+ int *p = (int *)0;
+ if (c) p = & a;
+ f(p);
+ /*@ check main_valid_ko: \valid(p); */ ;
+ /*@ check main_p_content_ko: *p ≡ 0; */ ;
+ loop();
+ __retres = 0;
+ return __retres;
+}
+
+void loop(void)
+{
+ int j = 0;
+ {
+ int i = 0;
+ /*@ check loop invariant false_but_preserved: j ≡ 10;
+ loop assigns i; */
+ while (i < 10) i ++;
+ }
+ /*@ check implied_by_false_invariant: j ≡ 10; */ ;
+ l: /*@ check invariant \true; */ ;
+ if (j >= 10) goto l1;
+ j ++;
+ goto l;
+ l1: ;
+ return;
+}
+
+
diff --git a/tests/spec/oracle/generalized_check.2.res.oracle b/tests/spec/oracle/generalized_check.2.res.oracle
deleted file mode 100644
index 7e0503ac2ae81e3733b87703e497dee35f843332..0000000000000000000000000000000000000000
--- a/tests/spec/oracle/generalized_check.2.res.oracle
+++ /dev/null
@@ -1,51 +0,0 @@
-[kernel] Parsing generalized_check.i (no preprocessing)
-/* Generated by Frama-C */
-/*@ check lemma easy_proof: \false;
- */
-/*@ check requires f_valid_x: \valid(x);
- check ensures f_init_x: *\old(x) ≡ 0;
- assigns *x;
- */
-void f(int *x)
-{
- /*@ check f_valid_ko: \valid(x); */ ;
- *x = 0;
- return;
-}
-
-void loop(void);
-
-int main(void)
-{
- int __retres;
- int volatile c;
- int a = 4;
- int *p = (int *)0;
- if (c) p = & a;
- f(p);
- /*@ check main_valid_ko: \valid(p); */ ;
- /*@ check main_p_content_ko: *p ≡ 0; */ ;
- loop();
- __retres = 0;
- return __retres;
-}
-
-void loop(void)
-{
- int j = 0;
- {
- int i = 0;
- /*@ check loop invariant false_but_preserved: j ≡ 10;
- loop assigns i; */
- while (i < 10) i ++;
- }
- /*@ check implied_by_false_invariant: j ≡ 10; */ ;
- l: /*@ check invariant \true; */ ;
- if (j >= 10) goto l1;
- j ++;
- goto l;
- l1: ;
- return;
-}
-
-
diff --git a/tests/spec/preprocess.c b/tests/spec/preprocess.c
index d22f2b661df4018473b9c1c0d9962cfa37c624d1..f0fffe879411fdcf440017be7e49ce147f2076af 100644
--- a/tests/spec/preprocess.c
+++ b/tests/spec/preprocess.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
DEPS: preprocess.h
OPT: -eva @EVA_OPTIONS@ -journal-disable -print
*/
diff --git a/tests/spec/shifts.c b/tests/spec/shifts.c
index 96e4eb6e8922a902b10d9f5986a5a0927f5d176b..1dffa076a0e9c16b8794f0a49d0795d2c2957fdc 100644
--- a/tests/spec/shifts.c
+++ b/tests/spec/shifts.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_OPTIONS@ -deps -journal-disable
*/
int e;
diff --git a/tests/spec/statement_behavior.c b/tests/spec/statement_behavior.c
index 2e462bd59fd128124fba41e5e5dec1cc788f1f3e..02551271d9e7eb7da938ec7026e539693397beb3 100644
--- a/tests/spec/statement_behavior.c
+++ b/tests/spec/statement_behavior.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_OPTIONS@ -inout -journal-disable
*/
diff --git a/tests/spec/test_config b/tests/spec/test_config
index c45a53fd4f24696d82ddcd3a0349cdc0da9e15cb..3451196c9530eca938c5827b1e4e89ed5d208693 100644
--- a/tests/spec/test_config
+++ b/tests/spec/test_config
@@ -3,8 +3,8 @@ COMMENT: we continue on annotation errors, as this allows to put
COMMENT: various variations of the same test in one file.
COMMENT: by default, no analysis is performed (since the PLUGIN directive
COMMENT: is empty).
-COMMENT: to perform value analyses, the macro @EVA_CONFIG@ (resp. @EVA_OPTIONS@)
+COMMENT: to perform value analyses, the macro @EVA_PLUGINS@ (resp. @EVA_OPTIONS@)
COMMENT: can be used into PLUGIN (resp. OPT) directives of specific test files.
PLUGIN:
-OPT: -pp-annot -print -kernel-warn-key=annot-error=active
+OPT: -pp-annot -print -kernel-warn-key=annot-error=active -machdep x86_32
diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i
index f430d09a01a05ef77d0e44218e2b91ee6ae41b79..b75fab0239da333ea63f0fcbe260c6551fb53de5 100644
--- a/tests/syntax/Refresh_visitor.i
+++ b/tests/syntax/Refresh_visitor.i
@@ -1,5 +1,5 @@
/* run.config
-PLUGIN: @EVA_CONFIG@
+PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
STDOPT: +"-no-print" +"@EVA_OPTIONS@"
*/
diff --git a/tests/syntax/copy_logic.i b/tests/syntax/copy_logic.i
index e8d51f637c43979535250512df04fb691d6f3139..092c056971cbbc42c4ff6ef2f6761210b5b1b980 100644
--- a/tests/syntax/copy_logic.i
+++ b/tests/syntax/copy_logic.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-copy" +"-eva"
*/
diff --git a/tests/syntax/copy_visitor.i b/tests/syntax/copy_visitor.i
index 773d4d977124a79c448bed69bf0e77bf6677853f..733edcfe34a43c5e9db532dfe280f2f2ee55be15 100644
--- a/tests/syntax/copy_visitor.i
+++ b/tests/syntax/copy_visitor.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-copy -eva @EVA_OPTIONS@"
*/
struct S {
diff --git a/tests/syntax/cpp-command.c b/tests/syntax/cpp-command.c
index dcda53f027bd0131b11c92ffe20db6b71ce1afa8..17a90fb779652ef9433d7da1bf261851c13aff3b 100644
--- a/tests/syntax/cpp-command.c
+++ b/tests/syntax/cpp-command.c
@@ -1,8 +1,8 @@
/* run.config*
FILTER: sed -e "s:/\(tmp\|var\|build\)/[^ ]*\.i:/tmp/FILE.i:g; s:$PWD:.:g; s:-I.*share/frama-c/share/libc:-I LIBC:g"
- OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
- OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
- OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\" \"using \\% has no effect : \$(basename \"\%input\")\""
- OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder"
- OPT: -no-autoload-plugins -print-cpp-commands
+ OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
+ OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
+ OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "printf \"%s\" \"using \\% has no effect : \$(basename \"\%input\")\""
+ OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder"
+ OPT: -machdep x86_32 -print-cpp-commands
*/
diff --git a/tests/syntax/extern_init.i b/tests/syntax/extern_init.i
index ff9d14ea9d08e78b4b04cbaf9083894b4234add4..320d115c3698d55ac7d70338fbd123adb4a58897 100644
--- a/tests/syntax/extern_init.i
+++ b/tests/syntax/extern_init.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
OPT: %{dep:@PTEST_NAME@_1.i} %{dep:@PTEST_NAME@_2.i} -eva @EVA_OPTIONS@
OPT: %{dep:@PTEST_NAME@_2.i} %{dep:@PTEST_NAME@_1.i} -eva @EVA_OPTIONS@
*/
diff --git a/tests/syntax/inline_calls.i b/tests/syntax/inline_calls.i
index e5ee646c97b2b0db8d9ef712a367b61feeee676b..d6f64104777bfad17212b1d93ff3bcfbb006ea22 100644
--- a/tests/syntax/inline_calls.i
+++ b/tests/syntax/inline_calls.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-inline-calls @all -kernel-msg-key printer:attrs"
STDOPT: +"-inline-calls @inline"
STDOPT: +"-inline-calls @inline -remove-inlined @inline"
diff --git a/tests/syntax/loop-case-switch-for-unroll.c b/tests/syntax/loop-case-switch-for-unroll.c
index a85d6181ce12201414a694847e730e1cdb50507d..48e667d7ffd7324f73e1fe8b1697d147a890a449 100644
--- a/tests/syntax/loop-case-switch-for-unroll.c
+++ b/tests/syntax/loop-case-switch-for-unroll.c
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-eva-slevel 100 -eva"
STDOPT: +"-ulevel 1 -eva-slevel 100 -eva"
STDOPT: +"-ulevel 2 -eva-slevel 100 -eva"
diff --git a/tests/syntax/no-print-libc-reparse.c b/tests/syntax/no-print-libc-reparse.c
index 2c73778b8eb7c4888bc01661cb61e2112bbb65c8..3bb87d76d198d836e4da4588091017f137e0d064 100644
--- a/tests/syntax/no-print-libc-reparse.c
+++ b/tests/syntax/no-print-libc-reparse.c
@@ -1,5 +1,5 @@
/*run.config
- STDOPT: #"-no-print-libc -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.c"
+ STDOPT: +"-no-print-libc -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.c"
*/
// tests that using -no-print-libc on a file with an enum produces output that
diff --git a/tests/syntax/oracle/unroll_visit.res.oracle b/tests/syntax/oracle/unroll_visit.res.oracle
index 8534230a58948226c4637db801458059b6f397f3..ad5ca987bd5532a8b747dc0afc31022df3af8a40 100644
--- a/tests/syntax/oracle/unroll_visit.res.oracle
+++ b/tests/syntax/oracle/unroll_visit.res.oracle
@@ -23,28 +23,29 @@
[inout] Inputs for function main:
\nothing
/* Generated by Frama-C */
+typedef char i8;
void main(void)
{
- int i = 0;
- if (! (i < 100)) goto unrolling_2_loop;
- i --;
+ i8 i = (char)0;
+ if (! ((int)i < 100)) goto unrolling_2_loop;
+ i = (i8)((int)i - 1);
/*@ assert i < 100; */ ;
- i ++;
- i ++;
+ i = (i8)((int)i + 1);
+ i = (i8)((int)i + 1);
unrolling_4_loop: ;
- if (! (i < 100)) goto unrolling_2_loop;
- i --;
+ if (! ((int)i < 100)) goto unrolling_2_loop;
+ i = (i8)((int)i - 1);
/*@ assert i < 100; */ ;
- i ++;
- i ++;
+ i = (i8)((int)i + 1);
+ i = (i8)((int)i + 1);
unrolling_3_loop: ;
/*@ loop pragma UNROLL 2;
loop pragma UNROLL "done", 2; */
- while (i < 100) {
- i --;
+ while ((int)i < 100) {
+ i = (i8)((int)i - 1);
/*@ assert i < 100; */ ;
- i ++;
- i ++;
+ i = (i8)((int)i + 1);
+ i = (i8)((int)i + 1);
}
unrolling_2_loop: ;
return;
diff --git a/tests/syntax/string_concat.c b/tests/syntax/string_concat.c
index b332b1392c6c141d0b5255b3097c81ca5f147204..2b0023ced8c1d64990f211c7ba5646d0d4d97376 100644
--- a/tests/syntax/string_concat.c
+++ b/tests/syntax/string_concat.c
@@ -1,6 +1,6 @@
/* run.config*
TIMEOUT: 600
-PLUGIN: @EVA_CONFIG@
+PLUGIN: @EVA_PLUGINS@
OPT: -eva
*/
#include <string.h>
diff --git a/tests/syntax/test_config b/tests/syntax/test_config
index e186e91c7e8dee9deee2b0ee66a1b39b4bb86e96..44df8c23bf474e289c90af7e416aa2fbbf00e400 100644
--- a/tests/syntax/test_config
+++ b/tests/syntax/test_config
@@ -2,9 +2,9 @@ COMMENT: this directory is meant to test exclusively the front-end
COMMENT: (parser, type-checker, linker, syntactic transformations).
COMMENT: by default, no analysis is performed since only the varadic plugin is
COMMENT: used.
-COMMENT: to perform value analyses, the macro @EVA_CONFIG@ (resp. @EVA_OPTIONS@)
+COMMENT: to perform value analyses, the macro @EVA_PLUGINS@ (resp. @EVA_OPTIONS@)
COMMENT: can be used into PLUGIN (resp. OPT) directives of specific test files.
PLUGIN: variadic
-OPT: -print
+OPT: -print -machdep x86_32
FILEREG:.*\.\(c\|i\|ci\)$
diff --git a/tests/syntax/unroll_labels.i b/tests/syntax/unroll_labels.i
index e4c089b91983b1ab7d59fc16694ee75a82673782..fd98bd531d6c7dbb0526048e690674eac6f82757 100644
--- a/tests/syntax/unroll_labels.i
+++ b/tests/syntax/unroll_labels.i
@@ -1,5 +1,5 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-eva @EVA_OPTIONS@"
STDOPT: +"-eva @EVA_OPTIONS@ -main main2 -eva-slevel 3"
*/
diff --git a/tests/syntax/unroll_visit.i b/tests/syntax/unroll_visit.i
index 0359d4f1eb41d723868745af4cb0220d4157b09a..0ce37b9a9440704374a7690699d5ce5a5b59f537 100644
--- a/tests/syntax/unroll_visit.i
+++ b/tests/syntax/unroll_visit.i
@@ -1,11 +1,11 @@
/* run.config
- PLUGIN: @EVA_CONFIG@
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-eva @EVA_OPTIONS@ -deps -out -input -deps"
*/
-
+typedef char i8; // ideally, pretty-printing should keep 'i8' for some casts
void main() {
/*@ loop pragma UNROLL 2; */
- for(int i=0; i<100; i++) {
+ for(i8 i=0; i<100; i++) {
i--;
//@ assert i<100;
i++;
diff --git a/tests/syntax/wstring_concat.c b/tests/syntax/wstring_concat.c
index 15cc31d5a722e4a6fea54e4da610a7fff014a5bc..cea5f67d3e5b4d875376188d7aa5cadce809b23a 100644
--- a/tests/syntax/wstring_concat.c
+++ b/tests/syntax/wstring_concat.c
@@ -1,6 +1,6 @@
/* run.config*
TIMEOUT: 600
-PLUGIN: @EVA_CONFIG@
+PLUGIN: @EVA_PLUGINS@
OPT: -eva
*/
#include <wchar.h>
diff --git a/tests/test_config b/tests/test_config
index 2f27f8ac4a362a398e88ddde33b837467451248b..9a493bd5e80a4c14580e018e9878bfbd5dd8f3d7 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,10 +1,11 @@
-COMMENT: macros @EVA_CONFIG@ (resp. @EVA_OPTIONS@) are usables in test files
-COMMENT: redefining the PLUGIN (resp. OPT) directives.
+COMMENT: macros @EVA_PLUGINS@ (resp. @EVA_OPTIONS@ and @EVA_CONFIG@) are usables
+COMMENT: in test files redefining the PLUGIN (resp. OPT) directives.
COMMENT: the PLUGIN directive sets automatically the @PLUGIN@ macro that can be
COMMENT: used into others PLUGIN directives in order to extend the parent list
COMMENT: of used plug'ins.
-MACRO: EVA_CONFIG from inout eva scope variadic
+MACRO: EVA_PLUGINS from inout eva scope variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
-PLUGIN: @EVA_CONFIG@
-OPT: -eva @EVA_OPTIONS@ -out -input -deps
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_apron b/tests/test_config_apron
index 0a0593f80f718f357e971b646f59f66553c78a1e..91f0ba7b07a9d3bc69020edadf9ebe866ead28e8 100644
--- a/tests/test_config_apron
+++ b/tests/test_config_apron
@@ -1,5 +1,6 @@
-MACRO: EVA_CONFIG from inout eva scope variadic
+MACRO: EVA_PLUGINS from inout eva scope variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains apron-octagon -eva-warn-key experimental=inactive
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
FILTER: diff %{dep:../oracle/@PTEST_ORACLE@}
-PLUGIN: @EVA_CONFIG@
-OPT: -eva @EVA_OPTIONS@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise
index 56a350cfa0360ca7f0a25fcc93cb97a3a59e9c7c..705f3d44db63628c6cfe6a53285e2a32ac28d301 100644
--- a/tests/test_config_bitwise
+++ b/tests/test_config_bitwise
@@ -1,5 +1,6 @@
-MACRO: EVA_CONFIG from inout eva scope variadic
+MACRO: EVA_PLUGINS from inout eva scope variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains bitwise
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
FILTER: diff %{dep:../oracle/@PTEST_ORACLE@}
-PLUGIN: @EVA_CONFIG@
-OPT: -eva @EVA_OPTIONS@ -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_equalities b/tests/test_config_equalities
index 5b83ffdc836d0ea703ac4385aa7c6d3802b249ae..5efc24a16cd215f1445548b0b26f19ff243f11ee 100644
--- a/tests/test_config_equalities
+++ b/tests/test_config_equalities
@@ -1,5 +1,6 @@
-MACRO: EVA_CONFIG from inout eva scope variadic
+MACRO: EVA_PLUGINS from inout eva scope variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains equality
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
FILTER: diff %{dep:../oracle/@PTEST_ORACLE@}
-PLUGIN: @EVA_CONFIG@
-OPT: -eva @EVA_OPTIONS@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_gauges b/tests/test_config_gauges
index 640f30d644fe011fc3090985f30fa5e4cbb2d38b..4e751c3d7d737cfe9d1c8787a208839a66f7635c 100644
--- a/tests/test_config_gauges
+++ b/tests/test_config_gauges
@@ -1,3 +1,4 @@
-MACRO: EVA_CONFIG from inout eva scope variadic
+MACRO: EVA_PLUGINS from inout eva scope variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains gauges
-OPT: -eva @EVA_OPTIONS@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_octagons b/tests/test_config_octagons
index 8907bdd533ef1d83f47a13a78449fadc1a0cb2fe..4646bdc386578adba5e59af91286fe583e5f17f2 100644
--- a/tests/test_config_octagons
+++ b/tests/test_config_octagons
@@ -1,5 +1,6 @@
-MACRO: EVA_CONFIG from inout eva scope variadic
+MACRO: EVA_PLUGINS from inout eva scope variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-domains octagon
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
FILTER: diff %{dep:../oracle/@PTEST_ORACLE@}
-PLUGIN: @EVA_CONFIG@
-OPT: -eva @EVA_OPTIONS@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index 0a91fa1aac921de48b77aef7f06885be9d570088..edb58b80081e86639faf6d89bf69f1222f9b2058 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -1,5 +1,6 @@
-MACRO: EVA_CONFIG from inout eva scope variadic
+MACRO: EVA_PLUGINS from inout eva scope variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains symbolic-locations
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
FILTER: diff %{dep:../oracle/@PTEST_ORACLE@}
-PLUGIN: @EVA_CONFIG@
-OPT: -eva @EVA_OPTIONS@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/const_typedef.i b/tests/value/const_typedef.i
index a6432e9474afed6908c4fb7d287f493c227c1503..a672647be760b5f78e1a969ce5ee8769b6d056e4 100644
--- a/tests/value/const_typedef.i
+++ b/tests/value/const_typedef.i
@@ -1,5 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -print -then -eva @EVA_OPTIONS@ -lib-entry -no-print
+ PLUGIN= inout eva
+ OPT: -machdep x86_32 -print -then -eva @EVA_CONFIG@ -lib-entry -no-print
*/
typedef int INT[3][3];
diff --git a/tests/value/div.i b/tests/value/div.i
index bbbc25443de39eb609cf8d697afc2f64d2c0789b..83c8c0e512ea065b5e3a12131dbdb660196b9d56 100644
--- a/tests/value/div.i
+++ b/tests/value/div.i
@@ -1,6 +1,6 @@
/* run.config*
- STDOPT: #"-load-module scope -eva-remove-redundant-alarms"
- OPT: -no-autoload-plugins -load-module eva,inout -rte -then -eva @EVA_OPTIONS@
+ STDOPT: #"-eva-remove-redundant-alarms"
+ OPT: -machdep x86_32 -rte -then -eva @EVA_OPTIONS@
*/
int X,Y,Z1,Z2,T,U1,U2,V,W1,W2;
int a,b,d1,d2,d0,e;
diff --git a/tests/value/empty_base.c b/tests/value/empty_base.c
index db17afc2c601af33b35d140ebde2f135989097f5..a1e08e2b7e0741f4c18b6cac0b635446cf67ed43 100644
--- a/tests/value/empty_base.c
+++ b/tests/value/empty_base.c
@@ -1,6 +1,6 @@
/* run.config*
EXIT: 1
- STDOPT: #"-machdep gcc_x86_32"
+ STDOPT: +"-machdep gcc_x86_32"
STDOPT:
*/
// the tests above must be done separately because both fail:
diff --git a/tests/value/precond2.c b/tests/value/precond2.c
index 8934d1a847bc9d6ae83471d08e664e65778a41fd..bc435ecf54dcff61d34d19529a4f2032d8a37435 100644
--- a/tests/value/precond2.c
+++ b/tests/value/precond2.c
@@ -1,8 +1,8 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -rte -then -eva @EVA_OPTIONS@ -then -report -report-print-properties
- OPT: -no-autoload-plugins -load-module from,inout,eva,report,rtegen -eva @EVA_OPTIONS@ -then -rte -then -report -report-print-properties
+ PLUGIN: @PLUGIN@ report
+ OPT: -machdep x86_32 -rte -then -eva @EVA_OPTIONS@ -then -report -report-print-properties
+ OPT: -machdep x86_32 -eva @EVA_OPTIONS@ -then -rte -then -report -report-print-properties
*/
-
// Fuse with precond.c when bts #1208 is solved
int x;
diff --git a/tests/value/redundant_alarms.c b/tests/value/redundant_alarms.c
index 4231c5c8984eb4f9e4e681c5ea826100abfb16ba..ad157c747f7c0f4342a6e5b045b7a8d5f6888b03 100644
--- a/tests/value/redundant_alarms.c
+++ b/tests/value/redundant_alarms.c
@@ -1,5 +1,5 @@
/* run.config*
- PLUGIN: @EVA_CONFIG@ slicing sparecode
+ PLUGIN: @EVA_PLUGINS@ slicing sparecode
OPT: @EVA_OPTIONS@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -eva-remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
**/