From 090aec98831d1f16526c7d1176f915662d84f3f4 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 22 Jan 2021 17:25:16 +0100
Subject: [PATCH] [Tests] preparation for the merge of master about the new
machdep
---
tests/builtins/big_local_array.i | 2 +-
tests/builtins/test_config | 3 +-
tests/builtins/test_config_apron | 2 +-
tests/builtins/test_config_bitwise | 2 +-
tests/builtins/test_config_equalities | 2 +-
tests/builtins/test_config_gauges | 2 +-
tests/builtins/test_config_octagons | 2 +-
tests/builtins/test_config_symblocs | 2 +-
tests/cil/mkBinOp.i | 2 +-
tests/cil/test_config | 2 +-
tests/constant_propagation/test_config | 4 +-
tests/float/sqrt.c | 2 +-
tests/impact/test_config | 2 +-
tests/journal/control2.c | 2 +-
tests/journal/intra.i | 2 +-
tests/libc/coverage.c | 2 +-
tests/libc/fc_libc.c | 4 +-
tests/libc/limits_h.c | 16 +-
tests/libc/more_gcc_builtins.c | 2 +-
tests/libc/stdlib_h.c | 2 +-
tests/libc/test_config | 2 +-
tests/misc/add_assigns.i | 2 +-
tests/misc/bts1347.i | 2 +-
tests/misc/obfuscate.c | 2 +-
tests/misc/pragma-pack.c | 6 +-
tests/misc/pragma_pack_zero.c | 4 +-
tests/more_wp/Makefile | 137 ------------------
tests/more_wp/TODO | 31 ----
tests/more_wp/bubblesort.c | 100 -------------
tests/more_wp/quicksort.c | 130 -----------------
tests/occurrence/test_config | 2 +-
tests/pdg/bts1194.c | 2 +-
tests/pdg/test_config | 2 +-
tests/pretty_printing/test_config | 2 +-
tests/ptests_config | 1 -
tests/rte/test_config | 2 +-
tests/rte/value_rte.c | 2 +-
tests/saveload/bool.c | 2 +-
tests/saveload/load_one.i | 2 +-
tests/scope/zones.c | 2 +-
tests/slicing/test_config | 4 +-
tests/spec/array_typedef.c | 2 +-
tests/spec/assigns_result.i | 2 +-
tests/spec/assigns_void.c | 2 +-
tests/spec/behavior_assert.c | 2 +-
tests/spec/default_assigns_bts0966.i | 2 +-
tests/spec/generalized_check.i | 2 -
tests/spec/logic_def.c | 2 +-
.../oracle/generalized_check.0.res.oracle | 71 ++++++---
.../oracle/generalized_check.1.res.oracle | 95 ++++++------
.../oracle/generalized_check.2.res.oracle | 51 -------
tests/spec/preprocess.c | 2 +-
tests/spec/shifts.c | 2 +-
tests/spec/statement_behavior.c | 2 +-
tests/spec/test_config | 4 +-
tests/syntax/Refresh_visitor.i | 2 +-
tests/syntax/copy_logic.i | 2 +-
tests/syntax/copy_visitor.i | 2 +-
tests/syntax/cpp-command.c | 10 +-
tests/syntax/extern_init.i | 2 +-
tests/syntax/inline_calls.i | 2 +-
tests/syntax/loop-case-switch-for-unroll.c | 2 +-
tests/syntax/no-print-libc-reparse.c | 2 +-
tests/syntax/oracle/unroll_visit.res.oracle | 27 ++--
tests/syntax/string_concat.c | 2 +-
tests/syntax/test_config | 4 +-
tests/syntax/unroll_labels.i | 2 +-
tests/syntax/unroll_visit.i | 6 +-
tests/syntax/wstring_concat.c | 2 +-
tests/test_config | 11 +-
tests/test_config_apron | 7 +-
tests/test_config_bitwise | 7 +-
tests/test_config_equalities | 7 +-
tests/test_config_gauges | 5 +-
tests/test_config_octagons | 7 +-
tests/test_config_symblocs | 7 +-
tests/value/const_typedef.i | 3 +-
tests/value/div.i | 4 +-
tests/value/empty_base.c | 2 +-
tests/value/precond2.c | 6 +-
tests/value/redundant_alarms.c | 2 +-
81 files changed, 230 insertions(+), 644 deletions(-)
delete mode 100644 tests/more_wp/Makefile
delete mode 100644 tests/more_wp/TODO
delete mode 100644 tests/more_wp/bubblesort.c
delete mode 100644 tests/more_wp/quicksort.c
delete mode 100644 tests/spec/oracle/generalized_check.2.res.oracle
diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index ce4500f78d0..0b931e1f1fe 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 05cba93b48e..6d3bfef2392 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 e5aae733192..365fdc8d48c 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 e5aae733192..365fdc8d48c 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 e5aae733192..365fdc8d48c 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 e5aae733192..365fdc8d48c 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 e5aae733192..365fdc8d48c 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 e5aae733192..365fdc8d48c 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 9ce55c13e65..4cd4dae8718 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 ac06bd8d772..3ef8de699a5 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 9b002f56c8c..f9f75f64390 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 da6743b0866..f1cfd10a543 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 c0e7feda3b5..39d00a53e25 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 2ef7bce9a8c..82bee121d27 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 11a12368cef..b06e6bb6884 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 0a63b6c3c76..e11d52b0330 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 116627e8711..cf60494482a 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 8b124df5a62..2c663b2c564 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 d3d023ac786..614aae666d6 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 ea1b69046d2..39d9378e90e 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 237f9df534a..25dfffeef8e 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 d829e673c47..62ee66d75b7 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 dab9a7d22db..d94078d86db 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 3efb19fac6f..d28ccfb42f9 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 4e930ec2580..2f1dbe59e2f 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 6a89215bebb..22f956bd3c3 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 ebedd46d8a2..00000000000
--- 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 c634c171f0f..00000000000
--- 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 74d383c4e63..00000000000
--- 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 cbb9f0fb0ce..00000000000
--- 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 f68b112eccd..029a71e6518 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 3a8043fdba9..aaa06aacad1 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 42a9ea00fb2..78c7757cadf 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 cb1129105e5..523c8ad970e 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 301ad30532e..581b0bbb0ab 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 d265e69bf9f..60080e46918 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 d614f1cd9aa..186136b4a70 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 776352ac0a5..200d545f557 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 a223064c22f..cb33a395e5a 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 7b3d2161b05..80fc7e30553 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 4ca5fca8bac..70059f8e01c 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 7882dfda139..a8273f59814 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 134947f6cd5..bfde0dde8bf 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 ba4f8a4ac52..6f993130b39 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 30c50494257..2e8732b4b64 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 c473d0d55d8..0bffe80560e 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 23ab2c81449..9f3a2f6a735 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 f309563f6bf..8448756e44a 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 33aea489a5e..f93e7228b40 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 60b7e824fa4..7e0503ac2ae 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 7e0503ac2ae..00000000000
--- 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 d22f2b661df..f0fffe87941 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 96e4eb6e892..1dffa076a0e 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 2e462bd59fd..02551271d9e 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 c45a53fd4f2..3451196c953 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 f430d09a01a..b75fab0239d 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 e8d51f637c4..092c056971c 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 773d4d97712..733edcfe34a 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 dcda53f027b..17a90fb7796 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 ff9d14ea9d0..320d115c369 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 e5ee646c97b..d6f64104777 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 a85d6181ce1..48e667d7ffd 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 2c73778b8eb..3bb87d76d19 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 8534230a589..ad5ca987bd5 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 b332b1392c6..2b0023ced8c 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 e186e91c7e8..44df8c23bf4 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 e4c089b9198..fd98bd531d6 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 0359d4f1eb4..0ce37b9a944 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 15cc31d5a72..cea5f67d3e5 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 2f27f8ac4a3..9a493bd5e80 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 0a0593f80f7..91f0ba7b07a 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 56a350cfa03..705f3d44db6 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 5b83ffdc836..5efc24a16cd 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 640f30d644f..4e751c3d7d7 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 8907bdd533e..4646bdc3865 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 0a91fa1aac9..edb58b80081 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 a6432e9474a..a672647be76 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 bbbc25443de..83c8c0e512e 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 db17afc2c60..a1e08e2b7e0 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 8934d1a847b..bc435ecf54d 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 4231c5c8984..ad157c747f7 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
**/
--
GitLab