diff --git a/src/plugins/aorai/tests/test_config b/src/plugins/aorai/tests/test_config
index 68cdb87e735aee9026598e4f773117fd73492efd..a8b69cddad62d729e3f14b0f752346eab1594a0d 100644
--- a/src/plugins/aorai/tests/test_config
+++ b/src/plugins/aorai/tests/test_config
@@ -1 +1,3 @@
+PLUGIN: aorai eva,from,scope report wp,rtegen
+MODULE: aorai_test
MACRO: PROVE_OPTIONS
diff --git a/src/plugins/aorai/tests/test_config_prove.in b/src/plugins/aorai/tests/test_config_prove.in
index 8875fe9a4de64611beee7a96c8a56fda2ff051ef..19d10644b0d9a441c1cbf9fa017c1ee6f3faf0a4 100644
--- a/src/plugins/aorai/tests/test_config_prove.in
+++ b/src/plugins/aorai/tests/test_config_prove.in
@@ -1 +1,3 @@
+PLUGIN: aorai eva,from,scope report wp,rtegen
+MODULE: aorai_test
MACRO: PROVE_OPTIONS @AORAI_WP_SHARE@ -aorai-test-prove-aux-spec
diff --git a/src/plugins/e-acsl/tests/test_config_ci.in b/src/plugins/e-acsl/tests/test_config_ci.in
index 9b58fc5a4a9550952da1aaca405d6aec67e4899c..3f61a9a95f6c298c32d76b9bc59425a1aba9e566 100644
--- a/src/plugins/e-acsl/tests/test_config_ci.in
+++ b/src/plugins/e-acsl/tests/test_config_ci.in
@@ -1,9 +1,14 @@
MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
MACRO: MACHDEP -machdep gcc_x86_64
MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -verbose 0
+
MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
+
MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
+
+PLUGIN: E_ACSL eva,scope,variadic rtegen
+
LOG: gen_@PTEST_NAME@.c
OPT: @GLOBAL@ @EACSL@ -then-last @EVA@ @EVENTUALLY@
FILTER:@SEDCMD@ -e "s|[a-zA-Z/\\]\+frama_c_project_e-acsl_[a-z0-9]*|PROJECT_FILE|" -e "s|$FRAMAC_SHARE|FRAMAC_SHARE|g" -e "s|../../share|FRAMAC_SHARE|g" -e "s|./share/e-acsl|FRAMAC_SHARE/e-acsl|g" -e "s|share/e-acsl|FRAMAC_SHARE/e-acsl|g"
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
index 045e0fac2c994cb0d4fe5edc094ed3ddfb5b5a62..6c7b2aca44643307f328535feb302172ef21c182 100644
--- a/src/plugins/e-acsl/tests/test_config_dev.in
+++ b/src/plugins/e-acsl/tests/test_config_dev.in
@@ -12,7 +12,9 @@ MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X
COMMENT: Default options for the frama-c invocation
MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0
-EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi
+PLUGIN: E_ACSL eva,scope,variadic rtegen
+
+EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c-exe@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@ @ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi
COMMENT: These next macros can be redefined in a test file
COMMENT: Define the following macro in a test to pass extra options to the frama-c invocation
diff --git a/src/plugins/instantiate/tests/test_config b/src/plugins/instantiate/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..e76859ce46eb70cae21c0221ee19cde81dda11f4
--- /dev/null
+++ b/src/plugins/instantiate/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: instantiate
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/with_value.i b/src/plugins/loop_analysis/tests/loop_analysis/with_value.i
index b030fa5e58dbcbe8a8d388fcc49097265f53ec38..66a5ec6025be62fb11852a4cd88c80cab1d764e4 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/with_value.i
+++ b/src/plugins/loop_analysis/tests/loop_analysis/with_value.i
@@ -1,7 +1,7 @@
/*run.config
-OPT: -no-autoload-plugins -load-module from,inout,loopanalysis,eva,scope -eva -eva-show-progress -then -loop
+PLUGIN: from,inout,loopanalysis,eva,scope
+OPT: -eva -eva-show-progress -then -loop
*/
-
void f1(int n) {
for (int i = 1; i < n+2; i++); // i IN [1..6] (6)
}
diff --git a/src/plugins/loop_analysis/tests/test_config b/src/plugins/loop_analysis/tests/test_config
index 4d0023c27475cdf9b242f862679fa8375c351218..f5a7fe2c3073d7012157044a16ee50637344ba4e 100644
--- a/src/plugins/loop_analysis/tests/test_config
+++ b/src/plugins/loop_analysis/tests/test_config
@@ -1 +1,2 @@
-OPT: -no-autoload-plugins -load-module loopanalysis -loop
+PLUGIN: loopanalysis
+OPT: -loop
diff --git a/src/plugins/markdown-report/tests/md/test_config b/src/plugins/markdown-report/tests/md/test_config
index 2d99fda9914fe40e3d6dad849ead724f9a88ec2e..a6de95a18b6e6ac762b8988ba15d90f1dd4ac8d4 100644
--- a/src/plugins/markdown-report/tests/md/test_config
+++ b/src/plugins/markdown-report/tests/md/test_config
@@ -1,2 +1,3 @@
+PLUGIN: eva,inout,scope markdown_report
CMD: @frama-c@ -eva @PTEST_FILE@ -mdr-gen md -mdr-date="now" -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.@PTEST_NUMBER@.md
LOG: @PTEST_NAME@.@PTEST_NUMBER@.md
diff --git a/src/plugins/markdown-report/tests/sarif/cwe125.c b/src/plugins/markdown-report/tests/sarif/cwe125.c
index 4e3013719a1b91a9d99f904c7fc30fc044683df5..be4e873fb8849e996300279cb3406d967de04147 100644
--- a/src/plugins/markdown-report/tests/sarif/cwe125.c
+++ b/src/plugins/markdown-report/tests/sarif/cwe125.c
@@ -4,8 +4,8 @@ EXECNOW: LOG @PTEST_NAME@.parse.log @frama-c@ @PTEST_FILE@ -save @PTEST_DIR@/res
EXECNOW: LOG @PTEST_NAME@.eva.log @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_parse.sav -eva -save @PTEST_DIR@/result/@PTEST_NAME@_eva.sav > @PTEST_DIR@/result/@PTEST_NAME@.eva.log
EXECNOW: LOG @PTEST_NAME@.sarif @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_eva.sav -then -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic
*/
-#include "__fc_builtin.h"
+#include "__fc_builtin.h"
#define LENGTH 10
int getValueFromArray(int *array, int len, int index) {
diff --git a/src/plugins/markdown-report/tests/sarif/libc.c b/src/plugins/markdown-report/tests/sarif/libc.c
index 2f7438beff35d307549bdbe6d896110fa98956c0..ebddde12484e96c3ce1921fe5432db3d83d87a5b 100644
--- a/src/plugins/markdown-report/tests/sarif/libc.c
+++ b/src/plugins/markdown-report/tests/sarif/libc.c
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
+ CMD: @frama-c@ -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
LOG: with-libc.sarif
OPT: -mdr-out @PTEST_DIR@/result/with-libc.sarif
LOG: without-libc.sarif
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
index 01038bb8a72d1d607ca386bebf1c5ed0289b8063..05cf14524c10a6fb740df19c593e92e62f0eb406 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
@@ -16,9 +16,11 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/cwe125.c -save tests/sarif/result/cwe125_parse.sav",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report tests/sarif/cwe125.c -save tests/sarif/result/cwe125_parse.sav",
"arguments": [
- "-check", "tests/sarif/cwe125.c", "-save",
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report",
+ "tests/sarif/cwe125.c", "-save",
"tests/sarif/result/cwe125_parse.sav"
],
"exitCode": 0,
@@ -26,21 +28,25 @@
},
{
"commandLine":
- "frama-c -check -load tests/sarif/result/cwe125_parse.sav -eva -save tests/sarif/result/cwe125_eva.sav",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -load tests/sarif/result/cwe125_parse.sav -eva -save tests/sarif/result/cwe125_eva.sav",
"arguments": [
- "-check", "-load", "tests/sarif/result/cwe125_parse.sav", "-eva",
- "-save", "tests/sarif/result/cwe125_eva.sav"
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report", "-load",
+ "tests/sarif/result/cwe125_parse.sav", "-eva", "-save",
+ "tests/sarif/result/cwe125_eva.sav"
],
"exitCode": 0,
"executionSuccessful": true
},
{
"commandLine":
- "frama-c -check -load tests/sarif/result/cwe125_eva.sav -then -mdr-out tests/sarif/result/cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -load tests/sarif/result/cwe125_eva.sav -then -mdr-out tests/sarif/result/cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
"arguments": [
- "-check", "-load", "tests/sarif/result/cwe125_eva.sav", "-then",
- "-mdr-out", "tests/sarif/result/cwe125.sarif", "-mdr-gen",
- "sarif", "-mdr-no-print-libc", "-mdr-sarif-deterministic"
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report", "-load",
+ "tests/sarif/result/cwe125_eva.sav", "-then", "-mdr-out",
+ "tests/sarif/result/cwe125.sarif", "-mdr-gen", "sarif",
+ "-mdr-no-print-libc", "-mdr-sarif-deterministic"
],
"exitCode": 0,
"executionSuccessful": true
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index 92989f9ff24ed46cd969d699cbe957a4e091c99f..09463aba3706bc50f7c4ddc224a7f773ee9389a6 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -16,9 +16,11 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/std_string.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out tests/sarif/result/std_string.sarif",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report tests/sarif/std_string.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out tests/sarif/result/std_string.sarif",
"arguments": [
- "-check", "tests/sarif/std_string.c", "-eva", "-then",
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report",
+ "tests/sarif/std_string.c", "-eva", "-then",
"-mdr-sarif-deterministic", "-mdr-gen", "sarif", "-mdr-out",
"tests/sarif/result/std_string.sarif"
],
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
index 2e65770160b67d52666d872c32c3ccff177cf6d1..1c47d708f582d55b6f2214609000909f832b3abe 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
@@ -16,12 +16,12 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-out tests/sarif/result/with-libc.sarif",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic tests/sarif/libc.c -mdr-out tests/sarif/result/with-libc.sarif",
"arguments": [
- "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
- "-load-module", "eva,from,scope,markdown_report", "-eva",
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
- "-mdr-sarif-deterministic", "-mdr-out",
+ "-mdr-sarif-deterministic", "tests/sarif/libc.c", "-mdr-out",
"tests/sarif/result/with-libc.sarif"
],
"exitCode": 0,
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
index b22b1bf8f4209a3f890c272cdee6d5470526ac48..0772f06e8dc221cd8bf486cbcd3a21702bf27055 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
@@ -16,12 +16,13 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-no-print-libc -mdr-out tests/sarif/result/without-libc.sarif",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic tests/sarif/libc.c -mdr-no-print-libc -mdr-out tests/sarif/result/without-libc.sarif",
"arguments": [
- "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
- "-load-module", "eva,from,scope,markdown_report", "-eva",
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
- "-mdr-sarif-deterministic", "-mdr-no-print-libc", "-mdr-out",
+ "-mdr-sarif-deterministic", "tests/sarif/libc.c",
+ "-mdr-no-print-libc", "-mdr-out",
"tests/sarif/result/without-libc.sarif"
],
"exitCode": 0,
diff --git a/src/plugins/markdown-report/tests/test_config b/src/plugins/markdown-report/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..d8bce8de28a2aa935d226e8561a3097808500d60
--- /dev/null
+++ b/src/plugins/markdown-report/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: eva,from,scope markdown_report
diff --git a/src/plugins/nonterm/tests/test_config b/src/plugins/nonterm/tests/test_config
index 91f0e5ec1ff948b34ba561fc9d7369be7fd38b87..521ad6d1a0c2ee0cdd8963bbf7f80c5a0f35f524 100644
--- a/src/plugins/nonterm/tests/test_config
+++ b/src/plugins/nonterm/tests/test_config
@@ -1 +1,2 @@
-OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -eva -eva-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2
+PLUGIN: from,inout,nonterm,scope
+OPT: -eva -eva-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2
diff --git a/src/plugins/report/tests/report/classify.c b/src/plugins/report/tests/report/classify.c
index 59d10572d66174086765df608e8473c6ad2c2f62..53068d1fb7a6bb272020cde4a7cf821693cf6e5b 100644
--- a/src/plugins/report/tests/report/classify.c
+++ b/src/plugins/report/tests/report/classify.c
@@ -1,5 +1,6 @@
/* run.config
- CMD: @frama-c@ -kernel-warn-key=annot-error=active -no-autoload-plugins -load-module wp,report -report-output @PTEST_RESULT@/classified.@PTEST_NUMBER@.json -wp -wp-msg-key shell
+ CMD: @frama-c@ -kernel-warn-key=annot-error=active -report-output @PTEST_RESULT@/classified.@PTEST_NUMBER@.json -wp -wp-msg-key shell
+PLUGIN: wp,rtegen,report
LOG: classified.@PTEST_NUMBER@.json
OPT: -wp-prover qed -report-unclassified-untried REVIEW -then -report-classify
EXIT: 1
@@ -18,7 +19,6 @@ EXIT: 1
int a ;
-
/*@
requires a >= 0 ;
ensures a > 0 ;
diff --git a/src/plugins/report/tests/report/csv.c b/src/plugins/report/tests/report/csv.c
index 536cfb432f2702af8035011868cad8ee785095d9..c9e27daea85800e65c791ee988974205ca027585 100644
--- a/src/plugins/report/tests/report/csv.c
+++ b/src/plugins/report/tests/report/csv.c
@@ -1,10 +1,10 @@
/* run.config
+PLUGIN: report from,inout,scope,eva
LOG: csv.csv
- OPT: -no-autoload-plugins -load-module from,inout,report,scope,eva -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -eva-remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -eva-slevel 1
+ OPT: -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -eva-remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -eva-slevel 1
COMMENT: first, do an analysis without any message, but check that the .csv is complete. Then, redo the analysis with value warnings. slevel 1 is just there to force Value to restart
*/
volatile v;
-
void main1(int x) {
int t[10];
int u[15];
diff --git a/src/plugins/report/tests/report/hyp.i b/src/plugins/report/tests/report/hyp.i
index e8181b82a7f38bea8a94a56acc0a8545eee610df..8c448f2f02063d8dfc837607137387266ff1841f 100644
--- a/src/plugins/report/tests/report/hyp.i
+++ b/src/plugins/report/tests/report/hyp.i
@@ -1,6 +1,6 @@
/* run.config
- OPT: -no-autoload-plugins -load-module report -load-script tests/report/one_hyp.ml
- OPT: -no-autoload-plugins -load-module report -load-script tests/report/several_hyps.ml
+ OPT: -load-script tests/report/one_hyp.ml
+ OPT: -load-script tests/report/several_hyps.ml
*/
void f(void);
diff --git a/src/plugins/report/tests/report/single.i b/src/plugins/report/tests/report/single.i
index 5f152e86922de3c4d21e6dd15371cf24d9b75e89..ee9b1b4359d8283a9ec3f48769c6e35c9462127d 100644
--- a/src/plugins/report/tests/report/single.i
+++ b/src/plugins/report/tests/report/single.i
@@ -1,7 +1,7 @@
/* run.config
- OPT: -no-autoload-plugins -load-module report -load-script tests/report/projectified_status.ml
- OPT: -no-autoload-plugins -load-module report -load-script tests/report/no_hyp.ml
- OPT: -no-autoload-plugins -load-module report -load-script tests/report/multi_emitters.ml
+ OPT: -load-script tests/report/projectified_status.ml
+ OPT: -load-script tests/report/no_hyp.ml
+ OPT: -load-script tests/report/multi_emitters.ml
*/
void main() {
diff --git a/src/plugins/report/tests/test_config b/src/plugins/report/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..3c86d70370368197bb9b50d59a1557c9e37bf46a
--- /dev/null
+++ b/src/plugins/report/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: report
diff --git a/src/plugins/server/tests/batch/test_config b/src/plugins/server/tests/batch/test_config
index 4addf96dff82842ab79ae170fda242244765a7c0..38b36108cbd35f2b835cf9811ca9d0af06f960ab 100644
--- a/src/plugins/server/tests/batch/test_config
+++ b/src/plugins/server/tests/batch/test_config
@@ -1,2 +1,3 @@
+PLUGIN: server
LOG: @PTEST_NAME@.out.json
-OPT: -no-autoload-plugins -load-module server -check -server-batch @PTEST_DIR@/@PTEST_NAME@.json -server-batch-output-dir @PTEST_RESULT@ -server-msg-key use-relative-filepath
+OPT: -server-batch @PTEST_DIR@/@PTEST_NAME@.json -server-batch-output-dir @PTEST_RESULT@ -server-msg-key use-relative-filepath
diff --git a/src/plugins/studia/tests/test_config b/src/plugins/studia/tests/test_config
index dc79c97068c8125cbff6a916b7fed6d7b881d5f2..75c01a81568f5bd37820738e9a6fffd25798a21f 100644
--- a/src/plugins/studia/tests/test_config
+++ b/src/plugins/studia/tests/test_config
@@ -1 +1,2 @@
+PLUGIN: eva,inout,deps
OPT: -eva -journal-disable -out -input -deps
diff --git a/src/plugins/variadic/tests/known/print_libc.c b/src/plugins/variadic/tests/known/print_libc.c
index 265018f2c74c6d406a2f0b2e28e6866fe3dc03af..a7df6ff263a8daff3f836fa14a1d98b4e2e585ea 100644
--- a/src/plugins/variadic/tests/known/print_libc.c
+++ b/src/plugins/variadic/tests/known/print_libc.c
@@ -1,6 +1,7 @@
/* run.config
+PLUGIN: variadic
LOG: print_libc.pretty.c
- OPT: @PTEST_DIR@/empty.c -no-autoload-plugins -load-module variadic -no-print-libc -print -ocode @PTEST_DIR@/result/@PTEST_NAME@.pretty.c -then @PTEST_DIR@/result/@PTEST_NAME@.pretty.c
+ OPT: @PTEST_DIR@/empty.c -no-print-libc -print -ocode @PTEST_DIR@/result/@PTEST_NAME@.pretty.c -then @PTEST_DIR@/result/@PTEST_NAME@.pretty.c
*/
#include <stdio.h>
diff --git a/src/plugins/variadic/tests/test_config b/src/plugins/variadic/tests/test_config
index e076935b23463006f8f89ffcddb93f7f2748c691..e93c90a92be816e38e26da50679fb9e4a0a0fcb7 100644
--- a/src/plugins/variadic/tests/test_config
+++ b/src/plugins/variadic/tests/test_config
@@ -1 +1,2 @@
-OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -eva-slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print
+PLUGIN: variadic from,inout,eva,scope
+OPT: -print -kernel-verbose 0 -variadic-verbose 2 -eva -eva-slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print
diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config
index 51675fdbc52d819cf3c99c4480b3130bd0fa64f3..122bc50aadc0af5e1a21b2b2baf4703d6955ef59 100644
--- a/src/plugins/wp/tests/test_config
+++ b/src/plugins/wp/tests/test_config
@@ -1,2 +1,3 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-prover none -wp-print -wp-share ./share -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive"
+PLUGIN: wp
+CMD: @frama-c@ -wp -wp-prover none -wp-print -wp-share ./share -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive"
OPT:
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index f5f56f99251f2a4100444ab7bb74b0abc2128e07..f0225eb3f9a0c31d90b77761394778c3a2268793 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,2 +1,3 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+PLUGIN: wp
+CMD: @frama-c@ -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
OPT:
diff --git a/src/plugins/wp/tests/wp_acsl/checks.i b/src/plugins/wp/tests/wp_acsl/checks.i
index f3fdcbfcab8f623e1c5393ae7e7b4b977300a6c2..c55cf4d5c8907db89f1cb70eb449041ace623a33 100644
--- a/src/plugins/wp/tests/wp_acsl/checks.i
+++ b/src/plugins/wp/tests/wp_acsl/checks.i
@@ -1,14 +1,14 @@
/* run.config
- OPT: -eva -load-module scope,eva,report -then -report
+PLUGIN: wp,rtegen,scope,eva,report
+ OPT: -then -eva -then -report
+PLUGIN: wp,rtegen
OPT: -wp-prop=@check
OPT: -wp-prop=-@check
*/
/* run.config_qualif
- OPT: -load-module report -wp-steps 5 -then -report
+PLUGIN: wp,rtegen,report
+ OPT: -wp-steps 5 -then -report
*/
-
-// note: eva and wp gives the same reporting
-
//@ axiomatic A { predicate P reads \nothing ; }
void main() {
//@check c1: P;
@@ -17,3 +17,4 @@ void main() {
//@assert a2: P;
;
}
+// note: eva and wp gives the same reporting
diff --git a/src/plugins/wp/tests/wp_manual/manual.i b/src/plugins/wp/tests/wp_manual/manual.i
index 11a04e0783ab7854b9dcb873766eaa739de19bfa..9f3afd5d3ae753eb86fa336712f033cf4b64a825 100644
--- a/src/plugins/wp/tests/wp_manual/manual.i
+++ b/src/plugins/wp/tests/wp_manual/manual.i
@@ -4,6 +4,7 @@
/* run.config_qualif
OPT: -wp-msg-key shell @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap1.h
OPT: -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h
- OPT: -load-module report -kernel-verbose 0 -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report
+PLUGIN: wp,rtegen,report
+ OPT: -kernel-verbose 0 -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report
*/
void look_at_working_dir(void);
diff --git a/src/plugins/wp/tests/wp_plugin/nosession.i b/src/plugins/wp/tests/wp_plugin/nosession.i
index bb038ffd831fcb13d4ecbfeeef7154c92d576820..d1873a1222997221ed75c281b72bb3663ce61eeb 100644
--- a/src/plugins/wp/tests/wp_plugin/nosession.i
+++ b/src/plugins/wp/tests/wp_plugin/nosession.i
@@ -1,9 +1,9 @@
/* run.config
DONTRUN:
*/
-
/* run.config_qualif
- CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
+ CMD: @frama-c@ -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
+PLUGIN: wp,rtegen
OPT: -wp -wp-prover alt-ergo -wp-session shall_not_exists_dir -wp-cache offline -wp-no-cache-env
COMMENT: The session directory shall not be created
*/
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index 9a4824f460e97fc22bacd03aae895c0e4c6147eb..08ad6804231703160d824e710dd98a9abfbc47f0 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,7 +1,7 @@
/* run.config_qualif
- OPT: -load-module eva,scope -no-wp -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
+PLUGIN: wp,rtegen,eva,scope
+ OPT: -no-wp -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
*/
-
/* run.config
DONTRUN:
*/
diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config
index 57d4ae071a433f4d3cecca0d8a218c0557f02e6d..c85101d0b58d18ca145d6963a56e1163ad1a7a0e 100644
--- a/src/plugins/wp/tests/wp_region/test_config
+++ b/src/plugins/wp/tests/wp_region/test_config
@@ -1,3 +1,4 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp
+PLUGIN: wp,rtegen
+CMD: @frama-c@
LOG: @PTEST_NAME@/region/job.dot
OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job
diff --git a/src/plugins/wp/tests/wp_usage/save_load.i b/src/plugins/wp/tests/wp_usage/save_load.i
index 8e908e8b69636dbd586fb832035975253a0cb13f..72e3c2595a6d9d9bf219e0b22aa4cbe494b9cb4c 100644
--- a/src/plugins/wp/tests/wp_usage/save_load.i
+++ b/src/plugins/wp/tests/wp_usage/save_load.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -no-autoload-plugins -load-module wp -wp-warn-key pedantic-assigns=inactive -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@.sav.err
- CMD: @frama-c@ -no-autoload-plugins -load-module wp -load @PTEST_DIR@/@PTEST_NAME@.sav -wp-warn-key pedantic-assigns=inactive
+ EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -wp-warn-key pedantic-assigns=inactive -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@.sav.err
+ CMD: @frama-c@ -load @PTEST_DIR@/@PTEST_NAME@.sav -wp-warn-key pedantic-assigns=inactive
OPT: -print
OPT: -wp -wp-prover none -wp-print
*/
diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index 83bb0fda45a32a5472b6aed4986d7fd80fa2cc0b..7c0854e14ae028bfb36a286b0aff0c94f6139784 100644
--- a/tests/builtins/big_local_array.i
+++ b/tests/builtins/big_local_array.i
@@ -1,7 +1,9 @@
/* run.config*
+ PLUGIN: @EVA_PLUGINS@ report
OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report
MODULE: big_local_array_script
OPT: @EVA_OPTIONS@ -then-on prj -print -report
+ PLUGIN: @EVA_PLUGINS@
MODULE:
OPT: @EVA_OPTIONS@ -print -journal-disable -no-initialized-padding-locals -eva
*/
@@ -12,7 +14,7 @@ struct S {
};
int main () {
- struct S x[32] =
+ struct S x[32] =
{ [0] = { .a = { 1,2,3 }, .b = { [5] = 5, 6, 7 }},
[3] = { 0,1,2,3,.b = { [17]=17 } }
};
diff --git a/tests/builtins/test_config b/tests/builtins/test_config
index 365fdc8d48cbda0c83335a388b0cf9b0d7ceb848..0264f96531357bbcf6c3f754e378dae60f5d84b8 100644
--- a/tests/builtins/test_config
+++ b/tests/builtins/test_config
@@ -1,3 +1,4 @@
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 -machdep x86_32
-OPT: -eva @EVA_CONFIG@ -journal-disable -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/callgraph/issue_55_iter_over_unregistered_function.i b/tests/callgraph/issue_55_iter_over_unregistered_function.i
index a39e29e042e8c876ef5338610289c83d56478cd0..535d2f3c5494e545651504c2b5e5e0bf88018e1c 100644
--- a/tests/callgraph/issue_55_iter_over_unregistered_function.i
+++ b/tests/callgraph/issue_55_iter_over_unregistered_function.i
@@ -1,8 +1,8 @@
/* run.config
+PLUGIN: @PTEST_PLUGIN@ eva,scope,inout
COMMENT: Test call to Callgraph.Uses.iter_on_callers/callees (through Inout)
OPT: -inout
*/
-
/*@ assigns *p \from x; */
extern void f(int x, int *p);
diff --git a/tests/callgraph/no_fp_unsound_warning.i b/tests/callgraph/no_fp_unsound_warning.i
index f841a6e1821b5c00be834118f3cd6a8594a9c59f..dcb0da94e41ae1c1c33a964b1015767b78cb163b 100644
--- a/tests/callgraph/no_fp_unsound_warning.i
+++ b/tests/callgraph/no_fp_unsound_warning.i
@@ -1,8 +1,8 @@
/* run.config
+PLUGIN: @PTEST_PLUGIN@ eva,scope,inout
COMMENT: Test that callgraph users are warned about -cg-no-function-pointers
OPT: -cg-function-pointers -out
OPT: -cg-no-function-pointers -out
*/
-
void main() {
}
diff --git a/tests/callgraph/test_config b/tests/callgraph/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..0757d9602b453e52bac8b869d4f07371c66d6a89
--- /dev/null
+++ b/tests/callgraph/test_config
@@ -0,0 +1,5 @@
+PLUGIN: callgraph
+STDOPT:
+
+# COMMENT: Directive to add in your test file when using STDOPT:
+# COMMENT: PLUGIN: @PTEST_PLUGIN@ @EVA_PLUGINS@
diff --git a/tests/compliance/test_config b/tests/compliance/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2454128362a6b8b71db649b6d45f3baf2b6df496
--- /dev/null
+++ b/tests/compliance/test_config
@@ -0,0 +1 @@
+PLUGIN:
diff --git a/tests/constant_propagation/bts117.c b/tests/constant_propagation/bts117.c
index 420cd12e426c82096ca8e4d57efc742b1e5258c8..5d0662f5a3382c3daa5aa7ce45acb44717853194 100644
--- a/tests/constant_propagation/bts117.c
+++ b/tests/constant_propagation/bts117.c
@@ -1,9 +1,13 @@
/* run.config
-OPT: -journal-disable -print
-OPT: -journal-disable -semantic-const-folding @EVA_OPTIONS@
-OPT: -journal-disable -sparecode-analysis @EVA_OPTIONS@
+PLUGIN:
+ OPT: -print
+PLUGIN: @CONSTANT_PROPAGATION_PLUGINS@
+ OPT: -semantic-const-folding @EVA_OPTIONS@
+PLUGIN: @PTEST_PLUGIN@ sparecode
+ OPT: -sparecode-analysis @EVA_OPTIONS@
*/
+
int main1 (void) {
int r ;
if (1) r = 0; else r = 2;
@@ -15,6 +19,7 @@ int main2 (void){
if (r) r = 0; else r = 2;
return r;
}
+
int main (void) {
int x1 = main1();
int x2 = main2();
diff --git a/tests/constant_propagation/const_propagate.c b/tests/constant_propagation/const_propagate.c
index 064fee49c0ef0e892a9850a3d8acc80e410265bb..2e5e3f728eb889020c6c3f66a94155cfb7eecb2b 100644
--- a/tests/constant_propagation/const_propagate.c
+++ b/tests/constant_propagation/const_propagate.c
@@ -1,9 +1,9 @@
/* run.config
- OPT: -eva @EVA_OPTIONS@ -deps -out -input -scf -journal-disable
- OPT: -scf @EVA_OPTIONS@ -cast-from-constant -semantic-const-fold add3 -main init -journal-disable
+PLUGIN: @CONSTANT_PROPAGATION_PLUGINS@ from inout
+ OPT: -eva @EVA_OPTIONS@ -deps -out -input -scf
+ OPT: -scf @EVA_OPTIONS@ -main init -journal-disable -cast-from-constant -semantic-const-fold add3
*/
-int x,y,z;
-int TAB[10];
+int x,y,z, TAB[10];
struct st { int a, b ; } s1, s2;
typedef struct st ST ;
void test_struct (void) {
diff --git a/tests/constant_propagation/oracle/bts117.1.res.oracle b/tests/constant_propagation/oracle/bts117.1.res.oracle
index d496d1cea9692624bbb6b2c2f995932ef05c64d9..a918171fe0348838a78e2a483c3ee8dc38bc022a 100644
--- a/tests/constant_propagation/oracle/bts117.1.res.oracle
+++ b/tests/constant_propagation/oracle/bts117.1.res.oracle
@@ -6,11 +6,11 @@
[eva:initial-state] Values of globals at initialization
[eva] computing for function main1 <- main.
- Called from tests/constant_propagation/bts117.c:19.
+ Called from tests/constant_propagation/bts117.c:24.
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/constant_propagation/bts117.c:20.
+ Called from tests/constant_propagation/bts117.c:25.
[eva] Recording results for main2
[eva] Done for function main2
[eva] Recording results for main
diff --git a/tests/constant_propagation/oracle/bts117.2.res.oracle b/tests/constant_propagation/oracle/bts117.2.res.oracle
index c4fe5b334c660df8b4797674fe3eb150bf073a10..493c47fa83c80699c7fe64a78162c6f389e49e39 100644
--- a/tests/constant_propagation/oracle/bts117.2.res.oracle
+++ b/tests/constant_propagation/oracle/bts117.2.res.oracle
@@ -6,11 +6,11 @@
[eva:initial-state] Values of globals at initialization
[eva] computing for function main1 <- main.
- Called from tests/constant_propagation/bts117.c:19.
+ Called from tests/constant_propagation/bts117.c:24.
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/constant_propagation/bts117.c:20.
+ Called from tests/constant_propagation/bts117.c:25.
[eva] Recording results for main2
[eva] Done for function main2
[eva] Recording results for main
diff --git a/tests/constant_propagation/test_config b/tests/constant_propagation/test_config
index c9ce20f05d9b350fd5d065e1d08f26e53fc065b6..b3a8965ab1afefa926424d9f4730c5832a90b05a 100644
--- a/tests/constant_propagation/test_config
+++ b/tests/constant_propagation/test_config
@@ -1 +1,3 @@
+MACRO: CONSTANT_PROPAGATION_PLUGINS constant_propagation eva,scope
+PLUGIN: @CONSTANT_PROPAGATION_PLUGINS@
OPT: -journal-disable -scf @EVA_OPTIONS@ -machdep x86_32
diff --git a/tests/dynamic/test_config b/tests/dynamic/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2454128362a6b8b71db649b6d45f3baf2b6df496
--- /dev/null
+++ b/tests/dynamic/test_config
@@ -0,0 +1 @@
+PLUGIN:
diff --git a/tests/float/absorb.c b/tests/float/absorb.c
index a71117b1674d5f6ba2b6dc97aeacd836c6f275cd..dbc2c9be16eb08e8623adacb43484cee5e14f4b2 100644
--- a/tests/float/absorb.c
+++ b/tests/float/absorb.c
@@ -1,16 +1,16 @@
/* run.config
COMMENT: run.config is intentionally not-*
- EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err FRAMAC_PLUGIN=tests/.empty @frama-c@ -journal-disable -save @PTEST_DIR@/result/absorb.sav @PTEST_FILE@ > @PTEST_DIR@/result/absorb_sav.res 2> @PTEST_DIR@/result/absorb_sav.err
- EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load @PTEST_DIR@/result/absorb.sav -eva @EVA_CONFIG@ -journal-disable -float-hex -save @PTEST_DIR@/result/absorb.sav2 > @PTEST_DIR@/result/absorb_sav2.res 2> @PTEST_DIR@/result/absorb_sav2.err
+PLUGIN:
+ EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err @frama-c@ -save @PTEST_DIR@/result/absorb.sav @PTEST_FILE@ > @PTEST_DIR@/result/absorb_sav.res 2> @PTEST_DIR@/result/absorb_sav.err
+PLUGIN: @EVA_PLUGINS@
+ EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load @PTEST_DIR@/result/absorb.sav -eva @EVA_CONFIG@ -float-hex -save @PTEST_DIR@/result/absorb.sav2 > @PTEST_DIR@/result/absorb_sav2.res 2> @PTEST_DIR@/result/absorb_sav2.err
OPT: -load @PTEST_DIR@/result/absorb.sav2 -deps -out -input
*/
/* run.config*
DONTRUN:
*/
#include "__fc_builtin.h"
-
float x = 1.0, y = 0.0, z, t, min_f, min_fl, den;
-
void main() {
long long b = Frama_C_interval(-2000000001, 2000000001);
b = b * b;
diff --git a/tests/impact/test_config b/tests/impact/test_config
index c449d18f602ef2fe815b38e0f2cdc3d467e1c815..953d2049ccde9dd0f40d5b3d195c5e3eb371b070 100644
--- a/tests/impact/test_config
+++ b/tests/impact/test_config
@@ -1 +1,2 @@
-OPT: -journal-disable -impact-print @EVA_OPTIONS@
+PLUGIN: @EVA_PLUGINS@ impact
+OPT: -impact-print @EVA_OPTIONS@
diff --git a/tests/jcdb/jcdb.c b/tests/jcdb/jcdb.c
index 13af9552975e857f6e062cd3068b82e98d9a33bd..c35dc80b7bfb0406a6653fcd8891cb2d7063b2a4 100644
--- a/tests/jcdb/jcdb.c
+++ b/tests/jcdb/jcdb.c
@@ -5,7 +5,7 @@
OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -no-autoload-plugins
MODULE:
EXECNOW: LOG list_files.res LOG list_files.err share/analysis-scripts/list_files.py @PTEST_DIR@/compile_commands_working.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
- EXECNOW: LOG logic-pp-include.res LOG logic-pp-include.err @frama-c@ -json-compilation-database @PTEST_DIR@/logic-pp-include @PTEST_DIR@/logic-pp-include/no-stdio.c -print -no-autoload-plugins > @PTEST_DIR@/result/logic-pp-include.res 2> @PTEST_DIR@/result/logic-pp-include.err
+ EXECNOW: LOG logic-pp-include.res LOG logic-pp-include.err @frama-c@ -json-compilation-database @PTEST_DIR@/logic-pp-include @PTEST_DIR@/logic-pp-include/no-stdio.c -print > @PTEST_DIR@/result/logic-pp-include.res 2> @PTEST_DIR@/result/logic-pp-include.err
*/
#include <stdio.h>
diff --git a/tests/jcdb/test_config b/tests/jcdb/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2454128362a6b8b71db649b6d45f3baf2b6df496
--- /dev/null
+++ b/tests/jcdb/test_config
@@ -0,0 +1 @@
+PLUGIN:
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 71676ee94fde86777dcac52dfb32ac462dbeba74..274b87c862bf5786beffcb180565eb82d3ddda93 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,5 +1,6 @@
/* run.config
- MODULE: @PTEST_NAME@
+ PLUGIN: @EVA_PLUGINS@ sparecode
+ MODULE: @PTEST_NAME@
EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name tests/journal/result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null
CMD: @frama-c@
OPT: -load-script tests/journal/result/intra_journal -journal-disable
@@ -12,7 +13,6 @@
* slicing analysis removes statement having variables with
* prefix "spare_" and "any_"
*/
-
int G;
int tmp (int a) {
diff --git a/tests/journal/test_config b/tests/journal/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..5b4e9a8bdd2b7dce5f1cd2d18923ecc5f7519b56
--- /dev/null
+++ b/tests/journal/test_config
@@ -0,0 +1,2 @@
+PLUGIN:
+STDOPT:
diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index 342d79af62894d72d30d5a03c8e9c215baf37229..8f628572259c0844ff92bea687695c87757e4cd1 100644
--- a/tests/libc/coverage.c
+++ b/tests/libc/coverage.c
@@ -1,7 +1,7 @@
/* run.config*
+PLUGIN: @PTEST_PLUGIN@ metrics
OPT: -eva-no-builtins-auto @EVA_OPTIONS@ share/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
*/
-
#include "string.h"
void main() {
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 7b1e11d5a7fca2ade7f3553ea51e6200046fbac5..be7d334d64589f5c1a39a62f7ca4e09e0aea2dc7 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -1,6 +1,7 @@
/* run.config*
+ PLUGIN: @EVA_PLUGINS@ metrics
MODULE: check_libc_naming_conventions, check_const
- OPT: -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module metrics -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
+ OPT: -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
MODULE:
OPT: -print -print-libc -machdep x86_32
MODULE: check_parsing_individual_headers
@@ -151,7 +152,6 @@
#include "utmpx.h"
#include "wchar.h"
#include "wctype.h"
-
void main() {
/* The variables below must be const; otherwise the preconditions
and the assigns/from of some functions will not match */
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 7955573b0c8101d35d2a7b324dcc54e1a9266e80..28a573d0275225899c6d7d10046937e518c1b943 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -1,7 +1,4 @@
[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
-[kernel] :0: Warning: unnamed requires
-[kernel] share/libc/sys/socket.h:451: Warning:
- clause with '\initialized' must contain name 'initialization'
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -201,6 +198,9 @@
Function call = 98
Pointer dereferencing = 161
Cyclomatic complexity = 299
+[kernel] :0: Warning: unnamed requires
+[kernel] share/libc/sys/socket.h:451: Warning:
+ clause with '\initialized' must contain name 'initialization'
/* Generated by Frama-C */
#include "__fc_builtin.c"
#include "__fc_builtin.h"
diff --git a/tests/libc/test_config b/tests/libc/test_config
index cf5c5bb18359425ba47e530ac8c06c936f24d7e8..069a4888d38f81544d6797ecad65e1e1070e3198 100644
--- a/tests/libc/test_config
+++ b/tests/libc/test_config
@@ -1 +1,2 @@
+PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_CONFIG@ -cpp-extra-args='-nostdinc -Ishare/libc'
diff --git a/tests/metrics/test_config b/tests/metrics/test_config
index de6ff0089d8e793cb118e41d7cf4db48f4dfd3d6..b528a2dd90282d3f8f7655c1da9554b390f84662 100644
--- a/tests/metrics/test_config
+++ b/tests/metrics/test_config
@@ -1 +1,2 @@
-OPT: -no-autoload-plugins -load-module metrics,scope -metrics
+PLUGIN: metrics,scope
+OPT: -metrics
diff --git a/tests/misc/audit.c b/tests/misc/audit.c
index 094beded8fc1e0ed11bd9f1b31a8ffd134e870de..40a9e6b9f1b3e13039be451f6027cd259e0c055e 100644
--- a/tests/misc/audit.c
+++ b/tests/misc/audit.c
@@ -1,8 +1,8 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@
LOG: audit-out.json
STDOPT: #"-audit-check @PTEST_DIR@/audit-in.json -audit-prepare @PTEST_RESULT@/audit-out.json -kernel-warn-key audit=active"
*/
-
#include "audit_included.h"
#include "audit_included_but_not_listed.h"
diff --git a/tests/misc/booleans.i b/tests/misc/booleans.i
index 08cbc6cbd89c770448b363d827b620424faf1faa..224a393116b2932b4f29075fbb35705e354b3ca6 100644
--- a/tests/misc/booleans.i
+++ b/tests/misc/booleans.i
@@ -1,6 +1,8 @@
/*run.config
+PLUGIN: @EVA_PLUGINS@
OPT: -eva -print
*/
+
int main (void) {
int x = 42;
/*@ check (boolean)x == 17; */
diff --git a/tests/misc/bts0541.c b/tests/misc/bts0541.c
index 6bbabaaa30cadda796dfc7d69e53074fb4058368..a8dd2eebf5d3e4c744ef72e7eabf100b2c8241e2 100644
--- a/tests/misc/bts0541.c
+++ b/tests/misc/bts0541.c
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@
OPT: -pp-annot -cpp-extra-args="-I./share/libc" -pp-annot -eva @EVA_CONFIG@
*/
-
#include <stdbool.h>
#include <stdint.h>
#include <stdlib.h>
diff --git a/tests/misc/bts1201.i b/tests/misc/bts1201.i
index dda5727fbcd2222c91dcb711d8d75098afd97857..9f4c1d1506d94d42df8fd76ff4a6317639b94298 100644
--- a/tests/misc/bts1201.i
+++ b/tests/misc/bts1201.i
@@ -1,8 +1,11 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT: -eva-verbose 2 -print
*/
-void main() { //@ assert \true;
+
+void main() {
+ //@ assert \true;
}
void main2() {
diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i
index 2cb8c609baa0dfb5d506d7f24694408d1363f62e..f4f0441da5a6fc233463f202e6e1f8dee7175314 100644
--- a/tests/misc/bts1347.i
+++ b/tests/misc/bts1347.i
@@ -1,6 +1,13 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@ report
MODULE: @PTEST_NAME@
OPT: @EVA_OPTIONS@ -then -report
*/
-int f(int *x) { return *x; }
-int g(int *x) { return *(x++); }
+
+int f(int *x) {
+ return *x;
+}
+
+int g(int *x) {
+ return *(x++);
+}
diff --git a/tests/misc/change_main.i b/tests/misc/change_main.i
index 374658f38ce3c2823acdbe90a413a4b8e17deb55..49e603b43cdee671bad07b0047e70732f9dfa92e 100644
--- a/tests/misc/change_main.i
+++ b/tests/misc/change_main.i
@@ -1,6 +1,6 @@
/* run.config*
+ PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT: -eva -main f -then-on change_main -main g -eva
*/
-
int f(int x) { return x; }
diff --git a/tests/misc/char_ampamp.c b/tests/misc/char_ampamp.c
index aaa77b01d752f75c7487100266144678c766550b..ca336e60b0d24d6dfb1619fbc1e9f1d20f2b08eb 100644
--- a/tests/misc/char_ampamp.c
+++ b/tests/misc/char_ampamp.c
@@ -1,3 +1,8 @@
+/* run.config
+ PLUGIN: @EVA_PLUGINS@
+STDOPT:
+*/
+
char c=1;
int y;
diff --git a/tests/misc/ensures.i b/tests/misc/ensures.i
index 88df7e52cee82769532184b9ea77ea1b73d27644..876ba0671a7ffc352a9dab685b156152be9df7f2 100644
--- a/tests/misc/ensures.i
+++ b/tests/misc/ensures.i
@@ -1,6 +1,11 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT:
*/
+
+
//@ ensures *p==1;
-void main(int * p){ *p = 0; }
+void main(int * p) {
+ *p = 0;
+}
diff --git a/tests/misc/fam_with_init.i b/tests/misc/fam_with_init.i
index d7e8c5463b4468718e08c0388284d369ee08f7d5..72e16cb63b0b2b40dd11e64a6053fae0e56a64ca 100644
--- a/tests/misc/fam_with_init.i
+++ b/tests/misc/fam_with_init.i
@@ -1,7 +1,7 @@
/* run.config
-STDOPT: +"-print"
+PLUGIN: @EVA_PLUGINS@
+ STDOPT: +"-print"
*/
-
struct s {
int a;
char data[]; // FAM
diff --git a/tests/misc/function_ptr_alignof.i b/tests/misc/function_ptr_alignof.i
index 1f4b218d0bfd2f02b8e5d3e152eb1177fb4ddf75..deda78cccb535cb02e4055951cb34c12529b6f1f 100644
--- a/tests/misc/function_ptr_alignof.i
+++ b/tests/misc/function_ptr_alignof.i
@@ -1,9 +1,9 @@
/* run.config*
+PLUGIN: @EVA_PLUGINS@
EXIT: 1
STDOPT:
*/
-
void f(void) { }
int main(void)
diff --git a/tests/misc/function_ptr_lvalue_1.i b/tests/misc/function_ptr_lvalue_1.i
index b48ddbd09f7be85d24a13b2f581addd5a8a8fbae..3659b05aae347cae3631c649ef9e531f4d060b19 100644
--- a/tests/misc/function_ptr_lvalue_1.i
+++ b/tests/misc/function_ptr_lvalue_1.i
@@ -1,9 +1,9 @@
/* run.config*
+PLUGIN: @EVA_PLUGINS@
EXIT: 1
STDOPT:
*/
-
void f(void) {}
int main()
diff --git a/tests/misc/function_ptr_lvalue_2.i b/tests/misc/function_ptr_lvalue_2.i
index 333304c449f7728babafb3871439aa92bae480a3..a8e98ba4c41961fd96211487a1f5e990c9893a57 100644
--- a/tests/misc/function_ptr_lvalue_2.i
+++ b/tests/misc/function_ptr_lvalue_2.i
@@ -1,8 +1,8 @@
/* run.config*
+PLUGIN: @EVA_PLUGINS@
EXIT: 1
STDOPT:
*/
-
void f(void) {}
int main()
diff --git a/tests/misc/function_ptr_sizeof.i b/tests/misc/function_ptr_sizeof.i
index 36558b8808f5835948fe3bbe775dda0db517ad39..da0a6d2b8aebecdd7093f6127f843562df543e36 100644
--- a/tests/misc/function_ptr_sizeof.i
+++ b/tests/misc/function_ptr_sizeof.i
@@ -1,9 +1,9 @@
/* run.config*
+PLUGIN: @EVA_PLUGINS@
EXIT: 1
STDOPT:
*/
-
void f(void) { }
int main(void)
diff --git a/tests/misc/issue109.i b/tests/misc/issue109.i
index 4a6e475212ebf15e558888920e4c8e3600bc84fa..60b50daf93dd13b0f37f6a83faf4d3b9fcac4a2a 100644
--- a/tests/misc/issue109.i
+++ b/tests/misc/issue109.i
@@ -1,11 +1,17 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT: -eva @EVA_CONFIG@ -eva-slevel-function main:10
*/
+
void main() {
+
int i, j = 0;
+
for (i=0; i<10; i++) {
j++;
}
+
//@ assert i == j;
+
}
diff --git a/tests/misc/log-file.i b/tests/misc/log-file.i
index 498e4e0654ef12260798992d0ea71fcc66f73fd8..09a77cc462d57fc1678e9f1263f47bbdbece0569 100644
--- a/tests/misc/log-file.i
+++ b/tests/misc/log-file.i
@@ -6,6 +6,7 @@
LOG: log-file-value-all.txt
LOG: log-file-value-default.txt
LOG: plugin-log-all.txt
+PLUGIN: @EVA_PLUGINS@
STDOPT: #"-kernel-log w:@PTEST_RESULT@/log-file-kernel-warnings.txt,r:@PTEST_RESULT@/log-file-kernel-results.txt -eva-log f:@PTEST_RESULT@/log-file-feedback.txt,afewr:@PTEST_RESULT@/log-file-value-all.txt -eva-log :@PTEST_RESULT@/log-file-value-default.txt -then -kernel-log f:@PTEST_RESULT@/log-file-feedback.txt"
MODULE: plugin_log
OPT: -kernel-msg-key foo-category -kernel-log=a:@PTEST_RESULT@/plugin-log-all.txt
diff --git a/tests/misc/log_selfrec.i b/tests/misc/log_selfrec.i
index e7a647f6e453e88b9a63b844539f12d718e9cfbe..46e688a3e3faf0fd1daada2cb54d82835b03a70a 100644
--- a/tests/misc/log_selfrec.i
+++ b/tests/misc/log_selfrec.i
@@ -1,5 +1,5 @@
/* run.config*
-
+PLUGIN: report
EXIT: 1
OPT: -foobar -report-unclassified-error jazz
*/
diff --git a/tests/misc/log_twice.i b/tests/misc/log_twice.i
index 06a2ebcceeb318a91580fa7d4fb7bab6b922a72f..5a43817b8e49604810dddffb5a010641b79962ae 100644
--- a/tests/misc/log_twice.i
+++ b/tests/misc/log_twice.i
@@ -1,8 +1,8 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT: @EVA_CONFIG@
*/
-
int* f() {
int x;
return &x;
diff --git a/tests/misc/long_ident.c b/tests/misc/long_ident.c
index e0ebb31439ac8df4662bbc3106d93d620ff94a9b..58136fd73650e7c2a9171d569c57cf3a9c6e1600 100644
--- a/tests/misc/long_ident.c
+++ b/tests/misc/long_ident.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: obfuscator
OPT: -obfuscate -journal-disable
*/
diff --git a/tests/misc/obfuscate.c b/tests/misc/obfuscate.c
index f993479d0f78d337c57155e20dd3cddbf06a6228..0fb0323afb82e831788ae82bd525b0934b68d17f 100644
--- a/tests/misc/obfuscate.c
+++ b/tests/misc/obfuscate.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: obfuscator
OPT: -obfuscate
*/
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index b7d55c35d2b08c652da0b87c0ac9f06e6d2abe66..8c4217e9169d95b3ceb869fb45f8a1fd96ec8877 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -69,7 +69,7 @@
}
},
"sources": {
- "tests/misc/audit.c": "aec49f030fcf92bc135bd75e7088194f",
+ "tests/misc/audit.c": "f94ce1c8f5e5911260931783495e2c88",
"tests/misc/audit_included.h": "c2cc488143a476f69cf2ed04c3439e6e",
"tests/misc/audit_included_but_not_listed.h":
"c2cc488143a476f69cf2ed04c3439e6e"
diff --git a/tests/misc/oracle/audit.res.oracle b/tests/misc/oracle/audit.res.oracle
index 40464f54b363d2da4daa36ed357da2364c3f944e..6894ada7dc21fb8274b4aa5db6dd57ce025f0ecd 100644
--- a/tests/misc/oracle/audit.res.oracle
+++ b/tests/misc/oracle/audit.res.oracle
@@ -1,5 +1,5 @@
[kernel:audit] Warning:
- different hashes for tests/misc/audit.c: got aec49f030fcf92bc135bd75e7088194f, expected 01010101010101010101010101010101
+ different hashes for tests/misc/audit.c: got f94ce1c8f5e5911260931783495e2c88, expected 01010101010101010101010101010101
[kernel:audit] Warning:
different hashes for tests/misc/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list)
[kernel:audit] Warning:
diff --git a/tests/misc/oracle/booleans.res.oracle b/tests/misc/oracle/booleans.res.oracle
index 8f7927c6bceb80d83a27026a4ecd2ad4e9c7862b..fbf91d58dadbc18ce9f145ce98f9aaa7d2edc5e3 100644
--- a/tests/misc/oracle/booleans.res.oracle
+++ b/tests/misc/oracle/booleans.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/booleans.i:7: Warning: check got status invalid.
+[eva:alarm] tests/misc/booleans.i:9: Warning: check got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/tests/misc/oracle/bts1201.res.oracle b/tests/misc/oracle/bts1201.res.oracle
index 5d683d1decf911024bb296418d7fb0ea6661b50a..312abde0a4dbef5bb0cce723708e27bb0d10f80b 100644
--- a/tests/misc/oracle/bts1201.res.oracle
+++ b/tests/misc/oracle/bts1201.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/misc/bts1201.i:5: assertion got status valid.
+[eva] tests/misc/bts1201.i:8: assertion got status valid.
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
diff --git a/tests/misc/oracle/bts1347.res.oracle b/tests/misc/oracle/bts1347.res.oracle
index 63b1624064934b9b4fb599dc919fbe8c4e922b4e..bd052d2107e24b757eecbc4a414c8824ad152de7 100644
--- a/tests/misc/oracle/bts1347.res.oracle
+++ b/tests/misc/oracle/bts1347.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/bts1347.i:5: Warning:
+[eva:alarm] tests/misc/bts1347.i:8: Warning:
out of bounds read. assert \valid_read(x);
[eva] Recording results for f
[eva] done for function f
@@ -13,7 +13,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/bts1347.i:6: Warning:
+[eva:alarm] tests/misc/bts1347.i:12: Warning:
out of bounds read. assert \valid_read(tmp);
(tmp from x++)
[eva] Recording results for g
@@ -24,22 +24,22 @@
--- Properties of Function 'f'
--------------------------------------------------------------------------------
-[ Dead ] Assertion 'emitter' (file tests/misc/bts1347.i, line 5)
+[ Dead ] Assertion 'emitter' (file tests/misc/bts1347.i, line 8)
Locally valid, but unreachable.
By Eva because:
- - Unreachable return (file tests/misc/bts1347.i, line 5)
-[Unreachable] Unreachable return (file tests/misc/bts1347.i, line 5)
+ - Unreachable return (file tests/misc/bts1347.i, line 8)
+[Unreachable] Unreachable return (file tests/misc/bts1347.i, line 8)
by Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'g'
--------------------------------------------------------------------------------
-[ - ] Assertion 'Eva,mem_access' (file tests/misc/bts1347.i, line 6)
+[ - ] Assertion 'Eva,mem_access' (file tests/misc/bts1347.i, line 12)
tried with Eva.
-[ Partial ] Assertion 'emitter' (file tests/misc/bts1347.i, line 6)
+[ Partial ] Assertion 'emitter' (file tests/misc/bts1347.i, line 12)
By emitter, with pending:
- - Assertion 'Eva,mem_access' (file tests/misc/bts1347.i, line 6)
+ - Assertion 'Eva,mem_access' (file tests/misc/bts1347.i, line 12)
--------------------------------------------------------------------------------
--- Status Report Summary
@@ -55,9 +55,9 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/bts1347.i:5: Warning:
+[eva:alarm] tests/misc/bts1347.i:8: Warning:
out of bounds read. assert \valid_read(x);
-[eva] tests/misc/bts1347.i:5: assertion 'emitter' got status valid.
+[eva] tests/misc/bts1347.i:8: assertion 'emitter' got status valid.
[eva] Recording results for f
[eva] done for function f
[eva] Analyzing an incomplete application starting at g
@@ -65,9 +65,9 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/bts1347.i:6: Warning:
+[eva:alarm] tests/misc/bts1347.i:12: Warning:
out of bounds read. assert \valid_read(tmp);
(tmp from x++)
-[eva] tests/misc/bts1347.i:6: assertion 'emitter' got status valid.
+[eva] tests/misc/bts1347.i:12: assertion 'emitter' got status valid.
[eva] Recording results for g
[eva] done for function g
diff --git a/tests/misc/oracle/char_ampamp.res.oracle b/tests/misc/oracle/char_ampamp.res.oracle
index e48fc08714ecef939dbe64b842387547d45fee89..9b826050d9f6813368d462f3cbcf42717a2a6068 100644
--- a/tests/misc/oracle/char_ampamp.res.oracle
+++ b/tests/misc/oracle/char_ampamp.res.oracle
@@ -6,8 +6,8 @@
c ∈ {1}
y ∈ {0}
[eva] computing for function g <- main.
- Called from tests/misc/char_ampamp.c:12.
-[eva] tests/misc/char_ampamp.c:6: Frama_C_show_each_x: {1}
+ Called from tests/misc/char_ampamp.c:17.
+[eva] tests/misc/char_ampamp.c:11: Frama_C_show_each_x: {1}
[eva] Recording results for g
[eva] Done for function g
[eva] Recording results for main
diff --git a/tests/misc/oracle/ensures.res.oracle b/tests/misc/oracle/ensures.res.oracle
index ee0832cdeffc1cc003c4ae54db0a7947af527c57..395d3e8484bed83286957dc88b9227ac3313e961 100644
--- a/tests/misc/oracle/ensures.res.oracle
+++ b/tests/misc/oracle/ensures.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/ensures.i:5: Warning:
+[eva:alarm] tests/misc/ensures.i:8: Warning:
function main: postcondition got status invalid.
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
diff --git a/tests/misc/oracle/issue109.res.oracle b/tests/misc/oracle/issue109.res.oracle
index 6282ea4acd8c628f4af05e21d7bda570ddfb96c3..b31581fd4bb2e915ffde47bdaafa44636ea3b54b 100644
--- a/tests/misc/oracle/issue109.res.oracle
+++ b/tests/misc/oracle/issue109.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/misc/issue109.i:10: assertion got status valid.
+[eva] tests/misc/issue109.i:15: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -17,7 +17,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/misc/issue109.i:10: assertion got status valid.
+[eva] tests/misc/issue109.i:15: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/misc/oracle/well_typed_alarm.res.oracle b/tests/misc/oracle/well_typed_alarm.res.oracle
index cff9cdaaa88971d0ae07d576c88835d8e353efe0..5eaf869164e05b944de3f4d17b8ca5c8cc1947d5 100644
--- a/tests/misc/oracle/well_typed_alarm.res.oracle
+++ b/tests/misc/oracle/well_typed_alarm.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/well_typed_alarm.i:11: Warning:
+[eva:alarm] tests/misc/well_typed_alarm.i:16: Warning:
pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
diff --git a/tests/misc/pragma-pack.c b/tests/misc/pragma-pack.c
index b2e44f3f65464fb533c965f48beb09ce1d9be20a..0eda8ce2f0b4ba0a2e56bab74f6477e2ea5780b4 100644
--- a/tests/misc/pragma-pack.c
+++ b/tests/misc/pragma-pack.c
@@ -1,9 +1,9 @@
/*run.config
+ PLUGIN: @EVA_PLUGINS@
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"
#include <stdint.h>
diff --git a/tests/misc/pragma_pack_zero.c b/tests/misc/pragma_pack_zero.c
index 22f956bd3c37c453f011aee30726b8f443dfd79e..52c5a87ad91f6edc44b368af7a0119cd9402e5e6 100644
--- a/tests/misc/pragma_pack_zero.c
+++ b/tests/misc/pragma_pack_zero.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@
STDOPT: +"-machdep gcc_x86_64"
STDOPT: +"-machdep msvc_x86_64"
*/
@@ -7,7 +8,6 @@
// In GCC, its current (undocumented) behavior is equivalent to #pragma pack(),
// that is, disable packing (reset to default). We emulate this behavior,
// but with a warning.
-
#include "pragma-pack-utils.h"
#include <stdint.h>
diff --git a/tests/misc/test_config b/tests/misc/test_config
index 111c347883729eb88f73d71774c9496d687e21fb..2cfb7e2f9204e5c904f80f601742facf6608faaa 100644
--- a/tests/misc/test_config
+++ b/tests/misc/test_config
@@ -1,2 +1,7 @@
+PLUGIN:
MODULE: global_decl_loc
MODULE:
+STDOPT:
+
+# COMMENT: Directive to add in your test file when using STDOPT:
+# COMMENT: PLUGIN: @EVA_PLUGINS@
diff --git a/tests/misc/well_typed_alarm.i b/tests/misc/well_typed_alarm.i
index 11ac1cd00a1cd0e5ec6f93c00a59b6e0e3ecc00c..dcbe3dacc09f3599f32413e4ae8537b6c61b33b2 100644
--- a/tests/misc/well_typed_alarm.i
+++ b/tests/misc/well_typed_alarm.i
@@ -1,13 +1,19 @@
/* run.config*
+ PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT:
*/
+
int main(int c) {
+
int x = 0;
int y = 0;
+
int *p = &x;
int *q = &y;
+
if (c) q = &x;
if (p<=q) x++;
+
return *q;
}
diff --git a/tests/misc/widen_hints.c b/tests/misc/widen_hints.c
index fca1b6e7e6ef953b698c6d2fa04bee2193bd889c..0148d513d8cad7072b213dc38041fa8d3a85163e 100644
--- a/tests/misc/widen_hints.c
+++ b/tests/misc/widen_hints.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@
EXIT:1
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DSYNTAX_ERRORS -kernel-warn-key=annot-error=active
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DNONCONST
@@ -7,7 +8,6 @@
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DALLGLOBAL -eva-msg-key widen-hints
*/
#define N 2
-
const int x = 9;
int not_const = 42; // cannot be used as widen hint
diff --git a/tests/misc/widen_hints2.c b/tests/misc/widen_hints2.c
index bc457535df6b9a0d18e9f93e5a1767dbbaad438d..9d35092bfb98ff4599952dc315eac04772ee74de 100644
--- a/tests/misc/widen_hints2.c
+++ b/tests/misc/widen_hints2.c
@@ -1,8 +1,8 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
STDOPT: #"-eva-msg-key widen-hints"
OPT: -print
*/
-
#include <stdlib.h>
#define N 2
diff --git a/tests/misc/widen_hints_float.c b/tests/misc/widen_hints_float.c
index a01f0a357842a423528cc508dfc39663b307f0a8..13326812adfc4ab8d1637b3955172fc71a77cdff 100644
--- a/tests/misc/widen_hints_float.c
+++ b/tests/misc/widen_hints_float.c
@@ -1,8 +1,8 @@
/* run.config*
+ PLUGIN: @EVA_PLUGINS@
STDOPT: #"-eva-subdivide-non-linear 20"
*/
-
#include "__fc_builtin.h"
#include <math.h>
diff --git a/tests/misc/wstring_phase6.c b/tests/misc/wstring_phase6.c
index f9884778c87c760721d9a3f9616e909abe1f9ff0..c364cd912c972d11721d70b0295354cd5e22d3b5 100644
--- a/tests/misc/wstring_phase6.c
+++ b/tests/misc/wstring_phase6.c
@@ -1,9 +1,9 @@
/* run.config
+PLUGIN: variadic
MODULE: @PTEST_NAME@
OPT: -journal-disable -print -variadic-no-translation
*/
#include <stdio.h>
-
// See http://stackoverflow.com/questions/18102502/mixing-wide-and-narrow-string-literals-in-c
int main(){
printf( "%s\n", "123" "456" );
diff --git a/tests/occurrence/test_config b/tests/occurrence/test_config
index 5e291a6ae016a6564af7152faf5f6ea67f58a94f..54290ebd2d68ef9aecc5959967d39d46a61ec28b 100644
--- a/tests/occurrence/test_config
+++ b/tests/occurrence/test_config
@@ -1 +1,2 @@
-STDOPT: +"-load-module" +"occurrence" -"-eva" -"-out" -"-input" -"-deps" +"-occurrence-verbose 1"
+PLUGIN: eva,scope occurrence
+STDOPT: -"-eva" -"-out" -"-input" -"-deps" +"-occurrence-verbose 1"
diff --git a/tests/pdg/bts1194.c b/tests/pdg/bts1194.c
index baa829837c3a54216aac8310f110bc0ee53fb35d..37d50ee5443a96ae718e5d645d5540edaea18da3 100644
--- a/tests/pdg/bts1194.c
+++ b/tests/pdg/bts1194.c
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@ pdg slicing
STDOPT: +"-eva -inout -pdg -calldeps -deps -then -slice-return main -then-last -print @EVA_OPTIONS@"
*/
-
int Y, X;
volatile v;
diff --git a/tests/pdg/test_config b/tests/pdg/test_config
index d9d741191d10ade715f1080b42b4a421d0d5e4c1..1f84f4645e5d2c1d56c903c01d91046a298c11c2 100644
--- a/tests/pdg/test_config
+++ b/tests/pdg/test_config
@@ -1 +1,2 @@
-OPT: -journal-disable @EVA_OPTIONS@ -pdg-print -pdg-verbose 2
+PLUGIN: @EVA_PLUGINS@ pdg
+OPT: @EVA_OPTIONS@ -pdg-print -pdg-verbose 2
diff --git a/tests/pretty_printing/test_config b/tests/pretty_printing/test_config
index c43ca10542958476406623d6a34d4049fce20852..3ef00bad562303349e568b77920e4499cd980972 100644
--- a/tests/pretty_printing/test_config
+++ b/tests/pretty_printing/test_config
@@ -1,5 +1,6 @@
COMMENT: this directory is meant to test the parser and pretty-printer
COMMENT: the default option checks that pretty-printed code can be merged
COMMENT: with the original one
+PLUGIN:
CMD: FRAMAC_PLUGIN=tests/.empty @frama-c@
-OPT: @PTEST_FILE@ -print -journal-disable -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
+OPT: @PTEST_FILE@ -print -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
diff --git a/tests/rte/oracle/unspecified_sequence.res.oracle b/tests/rte/oracle/unspecified_sequence.res.oracle
index 3df3256fe5fa9550c8fbe3a96a7c7e8522fd9561..2d9f1c127532b318461b9faaeb99c1befaf198b5 100644
--- a/tests/rte/oracle/unspecified_sequence.res.oracle
+++ b/tests/rte/oracle/unspecified_sequence.res.oracle
@@ -4,15 +4,15 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
t[0..9] ∈ {0}
-[eva:alarm] tests/rte/unspecified_sequence.i:7: Warning:
+[eva:alarm] tests/rte/unspecified_sequence.i:12: Warning:
function main: precondition got status unknown.
[eva] computing for function f <- main.
- Called from tests/rte/unspecified_sequence.i:10.
+ Called from tests/rte/unspecified_sequence.i:15.
[eva] Recording results for f
[eva] Done for function f
-[eva] tests/rte/unspecified_sequence.i:11: Reusing old results for call to f
+[eva] tests/rte/unspecified_sequence.i:16: Reusing old results for call to f
[eva] computing for function f <- main.
- Called from tests/rte/unspecified_sequence.i:11.
+ Called from tests/rte/unspecified_sequence.i:16.
[eva] Recording results for f
[eva] Done for function f
[eva] Recording results for main
diff --git a/tests/rte/test_config b/tests/rte/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..8351f51e855ecf8f8f4951813caf7b5d2bdbc455
--- /dev/null
+++ b/tests/rte/test_config
@@ -0,0 +1,2 @@
+PLUGIN: rtegen
+STDOPT:
diff --git a/tests/rte/unspecified_sequence.i b/tests/rte/unspecified_sequence.i
index bf067c5a072b4f58f001aa60f53788177cf504ce..63e60f119cf1b11b66d6bd7f0736be514624a28a 100644
--- a/tests/rte/unspecified_sequence.i
+++ b/tests/rte/unspecified_sequence.i
@@ -1,3 +1,8 @@
+/* run.config
+ PLUGIN: @EVA_PLUGINS@
+ STDOPT:
+*/
+
unsigned long long f(int x) {
return 0;
}
diff --git a/tests/rte/value_rte.c b/tests/rte/value_rte.c
index 0587fca439d1864503ee51cac0cbafb41e217127..9d2ee91f6686a741f5b2dcb0fd5e23e0fad09c30 100644
--- a/tests/rte/value_rte.c
+++ b/tests/rte/value_rte.c
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: eva,scope rtegen report
OPT: -rte -then -eva @EVA_OPTIONS@ -then -report
*/
-
#include "stdio.h"
int main(){
diff --git a/tests/rte_manual/test_config b/tests/rte_manual/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..7455cf5899e3ce3e7270344ef8217b1c06f9f2ee
--- /dev/null
+++ b/tests/rte_manual/test_config
@@ -0,0 +1,2 @@
+PLUGIN: @EVA_PLUGINS@ rtegen
+STDOPT:
diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c
index f90635c4440b48bc7fdd4446bd6f9adadd8a22a6..f942a8cae78be9b6917f8909f0d2349e818aaee5 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 ./bin/toplevel.opt -save ./tests/saveload/result/bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ ./tests/saveload/bool.c > tests/saveload/result/bool_sav.res 2> tests/saveload/result/bool_sav.err
+ EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err @frama-c@ -save ./tests/saveload/result/bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ ./tests/saveload/bool.c > tests/saveload/result/bool_sav.res 2> tests/saveload/result/bool_sav.err
STDOPT: +"-load ./tests/saveload/result/bool.sav -out -input -deps"
STDOPT: +"-load ./tests/saveload/result/bool.sav -eva @EVA_OPTIONS@"
*/
diff --git a/tests/saveload/callbacks.i b/tests/saveload/callbacks.i
index b1fe21aabd15e996e1b84a7ba90ab7025dcd4cdb..672fc08788ee5ecc689372682a92e5814c3faa0e 100644
--- a/tests/saveload/callbacks.i
+++ b/tests/saveload/callbacks.i
@@ -1,5 +1,5 @@
/* run.config
- EXECNOW: LOG callbacks_initial.res LOG callbacks_initial.err BIN callbacks.sav ./bin/toplevel.opt tests/saveload/callbacks.i -out -calldeps -eva-show-progress -main main1 -save ./tests/saveload/result/callbacks.sav > ./tests/saveload/result/callbacks_initial.res 2> ./tests/saveload/result/callbacks_initial.err
+ EXECNOW: LOG callbacks_initial.res LOG callbacks_initial.err BIN callbacks.sav @frama-c@ tests/saveload/callbacks.i -out -calldeps -eva-show-progress -main main1 -save ./tests/saveload/result/callbacks.sav > ./tests/saveload/result/callbacks_initial.res 2> ./tests/saveload/result/callbacks_initial.err
STDOPT: +"-load ./tests/saveload/result/callbacks.sav -main main2 -then -main main3"
*/
diff --git a/tests/saveload/isset.c b/tests/saveload/isset.c
index 720c3d635f2f3bc362c24fe83422bf51766ddfa6..8cdfc876ef88218d1f1c70f547bd2254820fd3e2 100644
--- a/tests/saveload/isset.c
+++ b/tests/saveload/isset.c
@@ -1,5 +1,5 @@
/* run.config
- EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav ./bin/toplevel.opt -quiet -eva @EVA_OPTIONS@ -save tests/saveload/result/isset.sav tests/saveload/isset.c > ./tests/saveload/result/isset_sav.res 2> ./tests/saveload/result/isset_sav.err
+ EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav @frama-c@ -quiet -eva @EVA_OPTIONS@ -save tests/saveload/result/isset.sav tests/saveload/isset.c > ./tests/saveload/result/isset_sav.res 2> ./tests/saveload/result/isset_sav.err
STDOPT: +"-quiet -load ./tests/saveload/result/isset.sav"
STDOPT: +"-load ./tests/saveload/result/isset.sav"
STDOPT: +"-eva @EVA_OPTIONS@ -load ./tests/saveload/result/isset.sav"
diff --git a/tests/saveload/load_one.i b/tests/saveload/load_one.i
index 75dde3f72926e6957c0fdfb898dbd3c3ba37932d..6eb0a89c1bd111ae094950e02c6e9ad00eee110e 100644
--- a/tests/saveload/load_one.i
+++ b/tests/saveload/load_one.i
@@ -1,6 +1,7 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
+ PLUGIN: @EVA_PLUGINS@ sparecode
+ MODULE: @PTEST_NAME@
+ STDOPT:
*/
int G;
@@ -12,7 +13,6 @@ int f (int x, int y) {
int main (void) {
int a = 1;
int b = 1;
-
/*@ assert a == 1; */
f (0, 0); /* this call is useless : should be removed */
diff --git a/tests/saveload/multi_project.i b/tests/saveload/multi_project.i
index ab0d9a44fd15de6c80394627618705578bd54744..acdf9a01fe1bca09b9aa63049dca4f9180e00298 100644
--- a/tests/saveload/multi_project.i
+++ b/tests/saveload/multi_project.i
@@ -1,8 +1,8 @@
/* run.config
- EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/multi_project.sav @EVA_OPTIONS@ -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > tests/saveload/result/multi_project_sav.res 2> tests/saveload/result/multi_project_sav.err
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- STDOPT: +"-load ./tests/saveload/result/multi_project.sav -journal-disable"
- CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ PLUGIN: @EVA_PLUGINS@ constant_propagation
+ EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err @frama-c@ -save ./tests/saveload/result/multi_project.sav @EVA_OPTIONS@ -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > tests/saveload/result/multi_project_sav.res 2> tests/saveload/result/multi_project_sav.err
+ STDOPT: +"-load ./tests/saveload/result/multi_project.sav"
+ MODULE: @PTEST_NAME@
OPT: -eva @EVA_OPTIONS@
*/
int f(int x) {
diff --git a/tests/saveload/sparecode.i b/tests/saveload/sparecode.i
index 33d1776ddc1ace121e6c617062505c43b4219b3d..b82bea7578da014e9734244c1d6f95a0e62e3b30 100644
--- a/tests/saveload/sparecode.i
+++ b/tests/saveload/sparecode.i
@@ -1,9 +1,9 @@
/* run.config
- EXECNOW: BIN sparecode.sav LOG sparecode_sav.res LOG sparecode_sav.err ./bin/toplevel.opt -slicing-level 2 -slice-return main -eva-show-progress -save ./tests/saveload/result/sparecode.sav tests/saveload/sparecode.i -then-on 'Slicing export' -print > tests/saveload/result/sparecode_sav.res 2> tests/saveload/result/sparecode_sav.err
+ PLUGIN: @EVA_PLUGINS@ slicing
+ EXECNOW: BIN sparecode.sav LOG sparecode_sav.res LOG sparecode_sav.err @frama-c@ -slicing-level 2 -slice-return main -eva-show-progress -save ./tests/saveload/result/sparecode.sav tests/saveload/sparecode.i -then-on 'Slicing export' -print > tests/saveload/result/sparecode_sav.res 2> tests/saveload/result/sparecode_sav.err
STDOPT: +"-load ./tests/saveload/result/sparecode.sav"
*/
int G;
-
int f (int x, int y) {
G = y;
return x;
diff --git a/tests/saveload/test_config b/tests/saveload/test_config
index 1712a20359b38feaedc7a61eec51ffa3aebc9879..0fb1ff9fa15158c8174c8231a22976557eb4dd40 100644
--- a/tests/saveload/test_config
+++ b/tests/saveload/test_config
@@ -1 +1,2 @@
+PLUGIN: @EVA_PLUGINS@
OPT: @EVA_OPTIONS@
diff --git a/tests/scope/bts971.c b/tests/scope/bts971.c
index 24716e1928853c5f80851385f3bd06a00519ae20..968ca119f331972615296755979e780362adc72f 100644
--- a/tests/scope/bts971.c
+++ b/tests/scope/bts971.c
@@ -1,11 +1,11 @@
/* run.config
- MODULE: @PTEST_NAME@
- OPT: -journal-disable -then -main main2
+ PLUGIN: @EVA_PLUGINS@ pdg
+ MODULE: @PTEST_NAME@
+ OPT: -then -main main2
*/
/* bug 971: */
volatile foo;
int v;
-
void f1 () {
v += 1;
}
diff --git a/tests/scope/test_config b/tests/scope/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..55b824af6be4dcc6553df43fd37dc898a4e4845f
--- /dev/null
+++ b/tests/scope/test_config
@@ -0,0 +1,2 @@
+PLUGIN: @EVA_PLUGINS@
+STDOPT:
diff --git a/tests/scope/zones.c b/tests/scope/zones.c
index a79ee26271d24c6c32a36533d28bf6ea338440c4..b60b239a0fcd7922d9cee94203c6c2f1594f6630 100644
--- a/tests/scope/zones.c
+++ b/tests/scope/zones.c
@@ -1,9 +1,9 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@ pdg
MODULE: @PTEST_NAME@
- OPT: -eva @EVA_OPTIONS@ -journal-disable
+ OPT: -eva @EVA_OPTIONS@
*/
-
/* bin/viewer.opt -eva @PTEST_DIR@/@PTEST_NAME@.c */
int T [10];
diff --git a/tests/slicing/combine.i b/tests/slicing/combine.i
index 704851ba39349b0e151e4a225cdb9ef865970fc9..05589afc7c888447f562aa65a4c850539bb99790 100644
--- a/tests/slicing/combine.i
+++ b/tests/slicing/combine.i
@@ -1,6 +1,6 @@
/* run.config
+ PLUGIN: @PTEST_PLUGIN@ constant_propagation sparecode
MODULE: libSelect @PTEST_NAME@
-
OPT: @EVA_OPTIONS@ -deps
*/
diff --git a/tests/slicing/test_config b/tests/slicing/test_config
index 1c214a23023446fa86e655de311a60df62051ceb..9c7afdad731fc9fe8f51b8d9c0d1b68a6001ebf2 100644
--- a/tests/slicing/test_config
+++ b/tests/slicing/test_config
@@ -1,3 +1,4 @@
MODULE: libSelect libAnim
MODULE:
+PLUGIN: eva,scope,variadic slicing
OPT: @EVA_OPTIONS@ -machdep x86_32
diff --git a/tests/sparecode/bts334.i b/tests/sparecode/bts334.i
index f6af16f8c93874894790dd75e3ce64ab219f6464..f05a44ace82ecd919b5168fe6f219d4116ad420c 100644
--- a/tests/sparecode/bts334.i
+++ b/tests/sparecode/bts334.i
@@ -1,7 +1,8 @@
/*run.config
- STDOPT: +"-sparecode-debug 0 -main main_init -sparecode-analysis -sparecode-no-annot "
- STDOPT: +"-sparecode-debug 0 -main main_init -slice-pragma loop_body -then-on 'Slicing export' -print"
- STDOPT: +"-sparecode-debug 0 -main main_init -slice-pragma loop_body -calldeps -then-on 'Slicing export' -print"
+ STDOPT: +"-sparecode-debug 0 -main main_init -sparecode-analysis -sparecode-no-annot "
+PLUGIN: @PTEST_PLUGIN@ slicing
+ STDOPT: +"-sparecode-debug 0 -main main_init -slice-pragma loop_body -then-on 'Slicing export' -print"
+ STDOPT: +"-sparecode-debug 0 -main main_init -slice-pragma loop_body -calldeps -then-on 'Slicing export' -print"
*/
int kf ;
int k[2] ;
@@ -10,7 +11,6 @@ static int si[2] = {0, 0};
static int so[2] = {0, 0};
int f(int vi , int i )
{ int vo ;
-
{vo = so[i] / kf + k[i] * (vi - si[i]);
so[i] = vo;
si[i] = vi;
diff --git a/tests/sparecode/calls.i b/tests/sparecode/calls.i
index 91773f1b22e0e11e51ff9a4402e9dd6df50d3b3a..dd0c6996091af7f446143ccee7108a9cdf19b84a 100644
--- a/tests/sparecode/calls.i
+++ b/tests/sparecode/calls.i
@@ -1,9 +1,9 @@
/* run.config
STDOPT: +"-sparecode-analysis"
+PLUGIN: @PTEST_PLUGIN@ slicing
STDOPT: +"-slicing-level 2 -slice-return main -then-on 'Slicing export' -print"
*/
int G;
-
int f (int x, int y) {
G = y;
return x;
diff --git a/tests/sparecode/dead_code.i b/tests/sparecode/dead_code.i
index 327e62941abd01360bcb74cc728a34ed68931618..5f4165959ff68c54f907c1b6707611503792f28b 100644
--- a/tests/sparecode/dead_code.i
+++ b/tests/sparecode/dead_code.i
@@ -1,5 +1,6 @@
/* run.config
STDOPT: +"-sparecode"
+PLUGIN: @PTEST_PLUGIN@ slicing
STDOPT: +"-slicing-level 2 -slice-return main -then-on 'Slicing export' -print"
*/
diff --git a/tests/sparecode/glob_decls.i b/tests/sparecode/glob_decls.i
index abdf205de22a03d9dce5d76f5e67c2cffa3695f3..eb211f029f70d1e7a2720fe26d44691f7472aeaf 100644
--- a/tests/sparecode/glob_decls.i
+++ b/tests/sparecode/glob_decls.i
@@ -1,6 +1,7 @@
/* run.config
- STDOPT: +"-lib-entry -sparecode-analysis "
- STDOPT: +"-lib-entry -slice-pragma main -slice-return main -then-on 'Slicing export' -print"
+ STDOPT: +"-lib-entry -sparecode-analysis "
+PLUGIN: @PTEST_PLUGIN@ slicing
+ STDOPT: +"-lib-entry -slice-pragma main -slice-return main -then-on 'Slicing export' -print"
STDOPT: +"-sparecode-rm-unused-globals"
*/
@@ -18,7 +19,6 @@ Ps GPs;
typedef struct { int a; int b; } Ts2;
Ts2 S2;
-
typedef char Ts2bis;
Ts2bis C = 'a';
diff --git a/tests/sparecode/intra.i b/tests/sparecode/intra.i
index 65316cbe60af3abe7f2e18cfe00cf1bae48b6903..21f41c1d712ad71bb0ec0e4718acf2c335e91df0 100644
--- a/tests/sparecode/intra.i
+++ b/tests/sparecode/intra.i
@@ -1,11 +1,13 @@
/* run.config
STDOPT: +"-sparecode-analysis"
+PLUGIN: @PTEST_PLUGIN@ slicing
STDOPT: +"-sparecode-debug 0 -slicing-level 2 -slice-return main -then-last -print"
+PLUGIN: @SPARECODE_PLUGINS@
STDOPT: +"-sparecode-debug 0 -main main2 -sparecode-analysis"
+PLUGIN: @PTEST_PLUGIN@ slicing
STDOPT: +"-sparecode-debug 0 -main main2 -slice-return main2 -then-last -print"
STDOPT: +"-sparecode-debug 0 -main main2 -slice-return main2 -slice-assert f10 -then-last -print"
*/
-
/* Waiting for results such as:
* spare code analysis removes statements having variables with
* prefix "spare_"
@@ -13,9 +15,7 @@
* slicing analysis removes statement having variables with
* prefix "spare_" and "any_"
*/
-
int G;
-
int tmp (int a) {
int x = a;
//@ assert x == a ;
diff --git a/tests/sparecode/params.i b/tests/sparecode/params.i
index 26bb415eefc1cd598a97b4b0fe1957132d1d0cab..4fd2d1b6efdebd9eb7f0ea088e74a442bb2049ab 100644
--- a/tests/sparecode/params.i
+++ b/tests/sparecode/params.i
@@ -1,8 +1,8 @@
/* run.config
STDOPT: +"-sparecode-analysis"
+PLUGIN: @PTEST_PLUGIN@ slicing
STDOPT: +"-slicing-level 2 -slice-return main -then-last -print"
*/
-
/* This is an example from #529. 'y' in [main1] should be visible to get a
* compilable result. But unfortunatly, this leads to also select [b=1] in
* [main]. This should be enhanced... */
diff --git a/tests/sparecode/test_config b/tests/sparecode/test_config
index a9330dd48d062e0b27b9bb948a88af6f4250c17a..40e3a32e1141194ae21aebe0470c76bca948bc06 100644
--- a/tests/sparecode/test_config
+++ b/tests/sparecode/test_config
@@ -1 +1,3 @@
+MACRO: SPARECODE_PLUGINS @EVA_PLUGINS@ sparecode
+PLUGIN: @SPARECODE_PLUGINS@
OPT: -journal-disable @EVA_OPTIONS@ -sparecode-debug 1
diff --git a/tests/spec/array_typedef.c b/tests/spec/array_typedef.c
index 86387dcf4273550cd3a88f637d544008c16bacdb..88daa60d902d2501043d8f697ce6152c0c9f44e0 100644
--- a/tests/spec/array_typedef.c
+++ b/tests/spec/array_typedef.c
@@ -1,9 +1,9 @@
/*run.config
- OPT: -print -eva @EVA_CONFIG@ -journal-disable
+PLUGIN: eva, scope
+ OPT: -print -eva @EVA_CONFIG@
*/
#define IP_FIELD 4
typedef int ip_address[IP_FIELD];
-
typedef struct {
ip_address src;
int dst[IP_FIELD];
diff --git a/tests/spec/assigns_result.i b/tests/spec/assigns_result.i
index f850166909efe129536bc4b54cae90447f6dbaaa..55ebd04043412a8e6d2f9e9480b4c0bb94de85b5 100644
--- a/tests/spec/assigns_result.i
+++ b/tests/spec/assigns_result.i
@@ -1,8 +1,8 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-deps @EVA_OPTIONS@"
*/
int X,Y;
-
/*@ assigns \result;
assigns \exit_status;
*/
diff --git a/tests/spec/assigns_void.c b/tests/spec/assigns_void.c
index 6e70195b864bfe5bb5f5d6f5c48ae74d798d9fbf..36cfe99b1ec2643f87f63401a3361e8cfce14152 100644
--- a/tests/spec/assigns_void.c
+++ b/tests/spec/assigns_void.c
@@ -1,10 +1,10 @@
/* run.config
- OPT: -print -journal-disable -kernel-warn-key=annot-error=active
- OPT: -eva @EVA_CONFIG@ -main g -print -no-annot -journal-disable
+ OPT: -print -kernel-warn-key=annot-error=active
+PLUGIN: eva,scope
+ OPT: -eva @EVA_CONFIG@ -main g -print -no-annot
*/
//@ assigns *x;
void f(void *x);
-
void g() {
int y;
int* x = &y;
diff --git a/tests/spec/behavior_assert.c b/tests/spec/behavior_assert.c
index 2f5d7f9760516f5bb73dea22b220b91f2e07edc3..7d0ce3885199a400d456597f6083bdf51a3470c2 100644
--- a/tests/spec/behavior_assert.c
+++ b/tests/spec/behavior_assert.c
@@ -1,8 +1,8 @@
/* run.config
-OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable -lib-entry
-OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable
+PLUGIN: eva,from,inout,scope
+ OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable -lib-entry
+ OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable
*/
-
int e;
/*@
diff --git a/tests/spec/default_assigns_bts0966.i b/tests/spec/default_assigns_bts0966.i
index 6b4cd671eda66ecb86c8a548620127b06604a1e6..4e2abccd49e698ad4aa3fc57c1e3c48b5556d250 100644
--- a/tests/spec/default_assigns_bts0966.i
+++ b/tests/spec/default_assigns_bts0966.i
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: eva,scope
OPT: -eva -print
*/
-
int auto_states[4] ; // = { 1 , 0 , 0, 0 };
enum states {
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 06f74139cfb7854ec517df292b9ca720dbd9ceed..ec9786ea47fe132077767e2b02ceda89f6849843 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,10 +1,10 @@
/* run.config
-OPT: -eva -eva-use-spec f
-OPT: -print
+PLUGIN: eva,scope
+ OPT: -eva -eva-use-spec f
+PLUGIN:
+ OPT: -print
*/
-
/*@ check lemma easy_proof: \false; */ // should not be put in any environment
-
/*@ check requires f_valid_x: \valid(x);
assigns *x;
check ensures f_init_x: *x == 0;
diff --git a/tests/spec/kw.c b/tests/spec/kw.c
index e57a4869f38f02d6bb9c79f6e7c7b1b7139b50fc..c780af02c9dc6fbc09f6badafd206db025676aa0 100644
--- a/tests/spec/kw.c
+++ b/tests/spec/kw.c
@@ -1,3 +1,9 @@
+/* run.config
+COMMENT: eva plugin is required for the slevel annotation
+PLUGIN: eva
+ STDOPT:
+*/
+
typedef int assert;
assert behavior = 0;
diff --git a/tests/spec/logic_def.c b/tests/spec/logic_def.c
index a9050410d76999cd48d4168575d26b22c5760e8d..c01bfb9e61297a6a281ab144bdd7c3524a753d9a 100644
--- a/tests/spec/logic_def.c
+++ b/tests/spec/logic_def.c
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-eva -eva-verbose 2"
*/
-
//@ logic integer foo(int x) = x + 2 ;
int main() {
diff --git a/tests/spec/oracle/assigns_void.0.res.oracle b/tests/spec/oracle/assigns_void.0.res.oracle
index ad68c8cfaa692fac538086d5a4969b433d91fff7..4e730b46a501a71788c2a543b438e9ad4922a0dc 100644
--- a/tests/spec/oracle/assigns_void.0.res.oracle
+++ b/tests/spec/oracle/assigns_void.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/spec/assigns_void.c (with preprocessing)
-[kernel:annot-error] tests/spec/assigns_void.c:5: Warning:
+[kernel:annot-error] tests/spec/assigns_void.c:6: Warning:
Cannot use a pointer to void here. Ignoring specification of function f
/* Generated by Frama-C */
void f(void *x);
diff --git a/tests/spec/oracle/statement_behavior.res.oracle b/tests/spec/oracle/statement_behavior.res.oracle
index 355b543903f30f9c0f17481e84bf35b15329bd6a..75f55931501876f76e9cd706ac8856116d8a50ec 100644
--- a/tests/spec/oracle/statement_behavior.res.oracle
+++ b/tests/spec/oracle/statement_behavior.res.oracle
@@ -10,7 +10,7 @@
no \from part for clause 'assigns five_times;'
[eva:alarm] tests/spec/statement_behavior.c:17: Warning:
assertion got status unknown.
-[eva:alarm] tests/spec/statement_behavior.c:4: Warning:
+[eva:alarm] tests/spec/statement_behavior.c:5: Warning:
function pfsqopfc: postcondition got status unknown.
[eva:alarm] tests/spec/statement_behavior.c:18: Warning:
accessing uninitialized left-value. assert \initialized(&five_times);
diff --git a/tests/spec/preprocess.c b/tests/spec/preprocess.c
index 64b0e62aeec278a03dfd822ddc33e5f539566b1f..5047548c8ecacacc9a172e81fc4cd7f069841aa2 100644
--- a/tests/spec/preprocess.c
+++ b/tests/spec/preprocess.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: -eva @EVA_CONFIG@ -journal-disable -print
+PLUGIN: eva,scope
+ OPT: -eva @EVA_CONFIG@ -print
*/
-
// see bts 1357
#define assert(x) (x)?1:0
diff --git a/tests/spec/shifts.c b/tests/spec/shifts.c
index a7d934e68da3bb28a16e8b0922eb34cc823694dc..5979c3d67ff3dc7feb1a1da0a3728bef50dc1ab6 100644
--- a/tests/spec/shifts.c
+++ b/tests/spec/shifts.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: -eva @EVA_CONFIG@ -deps -journal-disable
+PLUGIN: eva,scope,from
+ OPT: -eva @EVA_CONFIG@ -deps
*/
-
int e;
/*@
diff --git a/tests/spec/statement_behavior.c b/tests/spec/statement_behavior.c
index e91bc04723652701f7477a479ac8abf29fbacac5..c8834f72c8ea2102631e6060ac6dc0c3acc9cc3c 100644
--- a/tests/spec/statement_behavior.c
+++ b/tests/spec/statement_behavior.c
@@ -1,11 +1,11 @@
/* run.config
- OPT: -eva @EVA_CONFIG@ -inout -journal-disable
+PLUGIN: eva,inout,scope
+ OPT: -eva @EVA_CONFIG@ -inout
*/
/*@ ensures \result == (int)(5 * x);
*/
int pfsqopfc(int x) {
int five_times;
-
/*@
assigns five_times;
ensures five_times == (int)(5 * x);
diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i
index 6bf2f55e42ef1cd1009a5f8de7b7962f3349a710..c1d19f0a1d62fa1dd8b3d2f9befaaf2872fd4b25 100644
--- a/tests/syntax/Refresh_visitor.i
+++ b/tests/syntax/Refresh_visitor.i
@@ -1,8 +1,8 @@
/* run.config
+ PLUGIN: eva,scope
MODULE: @PTEST_NAME@
OPT: @EVA_OPTIONS@
*/
-
struct S { int i; };
/*@ lemma foo: \forall struct S x; x.i >= 0 || x.i < 0; */
diff --git a/tests/syntax/char_is_unsigned.i b/tests/syntax/char_is_unsigned.i
index 771ea26e6800c6fac56c23f00561be16aeda4fce..02a2088fef3e3a4aa038f1bd41a176bd45e36cf1 100644
--- a/tests/syntax/char_is_unsigned.i
+++ b/tests/syntax/char_is_unsigned.i
@@ -1,6 +1,7 @@
/* run.config
+PLUGIN: rtegen
MODULE: machdep_char_unsigned
- OPT:-print -machdep unsigned_char -then -constfold -rte
+ OPT: -print -machdep unsigned_char -then -constfold -rte
*/
char t[10];
diff --git a/tests/syntax/copy_logic.i b/tests/syntax/copy_logic.i
index 271bdce7af4fbd5e66c5393e3a7078be00677bbc..fee16b6120468fa4170798dc4290114348c9ee3d 100644
--- a/tests/syntax/copy_logic.i
+++ b/tests/syntax/copy_logic.i
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-copy" +"-eva"
*/
-
/*@ predicate p(int x); */
/*@ predicate q(int x) = x == 42; */
/*@ logic int f (int y); */
diff --git a/tests/syntax/copy_visitor.i b/tests/syntax/copy_visitor.i
index 2f475d79ae7a5ebeaf572e79e97e4b5f533cc833..d2d4bdb124e786dd2ee04327d9803b86b6c3dbe7 100644
--- a/tests/syntax/copy_visitor.i
+++ b/tests/syntax/copy_visitor.i
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-copy -eva @EVA_CONFIG@"
*/
struct S {
@@ -6,7 +7,6 @@ struct S {
int b;
};
struct S s = {.a = 1, .b=2};
-
/*@
requires \valid(s);
assigns s->a;
diff --git a/tests/syntax/copy_visitor_bts_1073.c b/tests/syntax/copy_visitor_bts_1073.c
index ec7e1ab180571bc3edbdc5ddafa90c2a602d0b21..e028f3cbe4d7e4d22d360e84786dad8c073e43e7 100644
--- a/tests/syntax/copy_visitor_bts_1073.c
+++ b/tests/syntax/copy_visitor_bts_1073.c
@@ -1,10 +1,10 @@
/* run.config
+PLUGIN: variadic
MODULE: @PTEST_NAME@
OPT:
MODULE: @PTEST_NAME@_bis
OPT: -test -then-on filtered -print
*/
-
#include "stdio.h"
int f(int x);
diff --git a/tests/syntax/cpp-command.c b/tests/syntax/cpp-command.c
index 3b9d41a71f080ea682cbc3482fa8412e53af2064..48585271169f5f929f117075c3011689e3011168 100644
--- a/tests/syntax/cpp-command.c
+++ b/tests/syntax/cpp-command.c
@@ -1,10 +1,10 @@
/* run.config*
FILTER: sed "s:/[^ ]*[/]cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::g; s: -m32::"
- OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
- OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
- OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
- OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder"
- OPT: -machdep x86_32 -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\n\" \"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
OPT: -cpp-extra-args-per-file=@PTEST_FILE@:"-DPF=\\\"cp%02d_3f\\\"" -no-autoload-plugins @PTEST_FILE@ -print
*/
diff --git a/tests/syntax/extern_init.i b/tests/syntax/extern_init.i
index e6773ed70089a517ab8a9499fbeb5b1b49304902..37a97faef54b721dcfc5c135e34f9c294e4c7235 100644
--- a/tests/syntax/extern_init.i
+++ b/tests/syntax/extern_init.i
@@ -1,7 +1,9 @@
/* run.config
+PLUGIN: eva,scope
OPT: @PTEST_DIR@/@PTEST_NAME@_1.i @PTEST_DIR@/@PTEST_NAME@_2.i -eva @EVA_CONFIG@
OPT: @PTEST_DIR@/@PTEST_NAME@_2.i @PTEST_DIR@/@PTEST_NAME@_1.i -eva @EVA_CONFIG@
*/
+
extern int a[] ;
/*@ assigns a[3] \from \nothing; */
diff --git a/tests/syntax/fct_ptr.i b/tests/syntax/fct_ptr.i
index 6b64b57479349ea4bb49e98aba19bcfce06789d3..63a57c55fdf6f3f53de8efb85cf41aa2a6aad003 100644
--- a/tests/syntax/fct_ptr.i
+++ b/tests/syntax/fct_ptr.i
@@ -1,20 +1,20 @@
-int f(int);
+/* run.config
+ PLUGIN: variadic
+ STDOPT:
+*/
+int f(int);
void *p = f;
-
int (*pf) (int x) = f;
-
int g() {
return ((int (*)(int))(*pf))(4);
}
-
int main () {
int (*q)(int) = (void *)0xfff45;
q(2);
q = p;
q(3);
}
-
typedef int (*Function_ptr)();
char *f_va(int a, ...) { return a; }
Function_ptr fp_table[1] = {(Function_ptr) f_va}; // warning, but no error
diff --git a/tests/syntax/function-types-compatible.i b/tests/syntax/function-types-compatible.i
index 770198b5691b45604630bd53effc937be6319407..a02b6ba9d748b2b9d10446148b7c43fd3f65c2bd 100644
--- a/tests/syntax/function-types-compatible.i
+++ b/tests/syntax/function-types-compatible.i
@@ -1,5 +1,12 @@
+/* run.config
+PLUGIN: variadic
+STDOPT:
+*/
+
void (*p)(int, ...);
+
void f();
+
void main() {
p = f;
p(1, 2); // warning, but no parsing error; will fail during execution
diff --git a/tests/syntax/gcc_builtins.c b/tests/syntax/gcc_builtins.c
index 00a9054c8b191a212b70e1b5000c4b710c4984ae..db5d0e38bdd1c27bea62b457f061eacbdb2c3211 100644
--- a/tests/syntax/gcc_builtins.c
+++ b/tests/syntax/gcc_builtins.c
@@ -1,7 +1,7 @@
/* run.config
+ PLUGIN: variadic
STDOPT: +"-machdep gcc_x86_32"
*/
-
#include "stdint.h"
#define likely(x) __builtin_expect((x),1)
diff --git a/tests/syntax/inline_calls.i b/tests/syntax/inline_calls.i
index a71073677d14b7d1b989f2d667f54b3d2bb917ac..4cf6b9c05992ba6000408bbe11dde27f4ad4bda0 100644
--- a/tests/syntax/inline_calls.i
+++ b/tests/syntax/inline_calls.i
@@ -1,9 +1,9 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-inline-calls @all -kernel-msg-key printer:attrs"
STDOPT: +"-inline-calls @inline"
STDOPT: +"-inline-calls @inline -remove-inlined @inline"
*/
-
int f() {
return 2;
}
diff --git a/tests/syntax/local-init-const.i b/tests/syntax/local-init-const.i
index 1d79724df761cbe3b412972bc0fb43c3fd156ea1..09793138d4693239a17072a39327874320e9e4ff 100644
--- a/tests/syntax/local-init-const.i
+++ b/tests/syntax/local-init-const.i
@@ -1,6 +1,8 @@
/*run.config
- OPT: -no-autoload-plugins -load-module eva,scope -eva -eva-verbose 0
+PLUGIN: eva,scope
+ OPT: -eva -eva-verbose 0
*/
+
unsigned id(unsigned x) { return x; }
void main() {
diff --git a/tests/syntax/loop-case-switch-for-unroll.c b/tests/syntax/loop-case-switch-for-unroll.c
index 7785be51b6a9e2495750bee02becb6c8fd846b61..3052cb9f5529fa6a77d6763f81aaee4673598cbd 100644
--- a/tests/syntax/loop-case-switch-for-unroll.c
+++ b/tests/syntax/loop-case-switch-for-unroll.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-eva-slevel 100 -eva"
STDOPT: +"-ulevel 1 -eva-slevel 100 -eva"
STDOPT: +"-ulevel 2 -eva-slevel 100 -eva"
@@ -6,7 +7,6 @@
the result of Frama-C piped to:
"| grep Frama_C_show_each | sed 's/^.*Frama_C_show_each_//'"
*/
-
#ifdef __FRAMAC__
#define print(line, s, a) Frama_C_show_each_ ## s ## _(a)
#else
diff --git a/tests/syntax/merge_variadic.i b/tests/syntax/merge_variadic.i
index dab33541e614a5c024f194ca824c8de30c0ffea6..b296224e959149e92dd12a8136ea5ed89d60076d 100644
--- a/tests/syntax/merge_variadic.i
+++ b/tests/syntax/merge_variadic.i
@@ -1,9 +1,9 @@
/* run.config
-OPT: @PTEST_DIR@/@PTEST_NAME@_aux.i -print
+PLUGIN: variadic
+ OPT: @PTEST_DIR@/@PTEST_NAME@_aux.i -print
*/
int open (const char* file, int flags, int mode) {
return -1;
}
-
/*@ assigns \result \from x; */
int foo (int x, int y);
diff --git a/tests/syntax/oracle/bts1553_2.res.oracle b/tests/syntax/oracle/bts1553_2.res.oracle
index 93dacee514969b19d8bc20ff47fcaffdd2a4c526..9293259fe565811c4e9f7f6dedc355b38faa4288 100644
--- a/tests/syntax/oracle/bts1553_2.res.oracle
+++ b/tests/syntax/oracle/bts1553_2.res.oracle
@@ -5,8 +5,6 @@
struct a {
int b ;
};
- /* compiler builtin:
- void Frama_C_show_aorai_state(...); */
/* compiler builtin:
__builtin_va_list __builtin_next_arg(void); */
/* compiler builtin:
@@ -42,8 +40,6 @@
struct a {
int b ;
};
- /* compiler builtin:
- void Frama_C_show_aorai_state(...); */
/* compiler builtin:
__builtin_va_list __builtin_next_arg(void); */
/* compiler builtin:
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index f81e5813ccc1c324160bc8600bf6e042c3e3fbbd..510a8f2b3ab41a3c39cd5c26cc41c8703528b9e1 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
@@ -2,8 +2,6 @@
[kernel:file:print-one]
result of parsing tests/syntax/check_builtin_bts1440.i:
/* Generated by Frama-C */
- void Frama_C_show_aorai_state(...);
-
void __builtin__Exit(int);
int __builtin___fprintf_chk(void *, int, char const * , ...);
diff --git a/tests/syntax/oracle/function-types-compatible.res.oracle b/tests/syntax/oracle/function-types-compatible.res.oracle
index 121d63a24e7721aba55611f25c673bf25953f32f..b25ea3698a6a3dd2d6995d583b96a878368f2cda 100644
--- a/tests/syntax/oracle/function-types-compatible.res.oracle
+++ b/tests/syntax/oracle/function-types-compatible.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/function-types-compatible.i (no preprocessing)
-[kernel:typing:incompatible-types-call] tests/syntax/function-types-compatible.i:4: Warning:
+[kernel:typing:incompatible-types-call] tests/syntax/function-types-compatible.i:11: Warning:
implicit conversion between incompatible function types:
void (*)()
and
diff --git a/tests/syntax/oracle/merge_variadic.res.oracle b/tests/syntax/oracle/merge_variadic.res.oracle
index 88885da35e2f84e1f548dd833903435f798a8958..a0c39aecf62846a1e8877d3a78f32647a8704355 100644
--- a/tests/syntax/oracle/merge_variadic.res.oracle
+++ b/tests/syntax/oracle/merge_variadic.res.oracle
@@ -3,7 +3,7 @@
[kernel:linker:drop-conflicting-unused] Warning:
Incompatible declaration for open:
different vararg specifiers
- First declaration was at tests/syntax/merge_variadic.i:4
+ First declaration was at tests/syntax/merge_variadic.i:5
Current declaration is at tests/syntax/merge_variadic_aux.i:5
Current declaration is unused, silently removing it
[kernel:linker:drop-conflicting-unused] Warning:
diff --git a/tests/syntax/oracle/static_formals_1.res.oracle b/tests/syntax/oracle/static_formals_1.res.oracle
index f3dc98b3d3003fb066ecc0db86d86140b90ce85c..6261380034edbdbaf53954bee958450e2f36d238 100644
--- a/tests/syntax/oracle/static_formals_1.res.oracle
+++ b/tests/syntax/oracle/static_formals_1.res.oracle
@@ -1,24 +1,24 @@
[kernel] Parsing tests/syntax/static_formals_1.c (with preprocessing)
[kernel] Parsing tests/syntax/static_formals_2.c (with preprocessing)
/* Generated by Frama-C */
-/*@ requires /* vid:26, lvid:26 */x < 10; */
-static int /* vid:60 */f(int /* vid:26, lvid:26 */x);
+/*@ requires /* vid:23, lvid:23 */x < 10; */
+static int /* vid:56 */f(int /* vid:23, lvid:23 */x);
-int /* vid:31 */g(void)
+int /* vid:28 */g(void)
{
- int /* vid:32 */tmp;
- /* vid:32 */tmp = /* vid:60 */f(4);
- return /* vid:32 */tmp;
+ int /* vid:29 */tmp;
+ /* vid:29 */tmp = /* vid:56 */f(4);
+ return /* vid:29 */tmp;
}
-/*@ requires /* vid:55, lvid:55 */x < 10; */
-static int /* vid:61 */f_0(int /* vid:55, lvid:55 */x);
+/*@ requires /* vid:51, lvid:51 */x < 10; */
+static int /* vid:57 */f_0(int /* vid:51, lvid:51 */x);
-int /* vid:58 */h(void)
+int /* vid:54 */h(void)
{
- int /* vid:59 */tmp;
- /* vid:59 */tmp = /* vid:61 */f_0(6);
- return /* vid:59 */tmp;
+ int /* vid:55 */tmp;
+ /* vid:55 */tmp = /* vid:57 */f_0(6);
+ return /* vid:55 */tmp;
}
diff --git a/tests/syntax/oracle/unroll_visit.res.oracle b/tests/syntax/oracle/unroll_visit.res.oracle
index 271518ba4c2d9a67a2fd616ca5818cbe5d4818b3..1679a9dc5d55a5b96376f47c9800d9501192aa9e 100644
--- a/tests/syntax/oracle/unroll_visit.res.oracle
+++ b/tests/syntax/oracle/unroll_visit.res.oracle
@@ -4,8 +4,8 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/syntax/unroll_visit.i:9: assertion got status valid.
-[eva] tests/syntax/unroll_visit.i:7: starting to merge loop iterations
+[eva] tests/syntax/unroll_visit.i:12: assertion got status valid.
+[eva] tests/syntax/unroll_visit.i:10: starting to merge loop iterations
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/syntax/oracle/variadic.res.oracle b/tests/syntax/oracle/variadic.res.oracle
index 9e0223986f0000922185c919e1881cb0f45c1bca..1052103bac84ae187ec185f26ae494a81c58d95d 100644
--- a/tests/syntax/oracle/variadic.res.oracle
+++ b/tests/syntax/oracle/variadic.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/variadic.i (no preprocessing)
-[kernel:typing:implicit-function-declaration] tests/syntax/variadic.i:20: Warning:
+[kernel:typing:implicit-function-declaration] tests/syntax/variadic.i:26: Warning:
Calling undeclared function f. Old style K&R code?
-[kernel:typing:no-proto] tests/syntax/variadic.i:21: Warning:
+[kernel:typing:no-proto] tests/syntax/variadic.i:27: Warning:
Calling function h that is declared without prototype.
Its formals will be inferred from actual arguments
/* Generated by Frama-C */
diff --git a/tests/syntax/static_formals_1.c b/tests/syntax/static_formals_1.c
index 6cd8687eba15553886326158692c69839fd4e061..97cfbca9a65701a0dfebf4cab8f8550af431ebbf 100644
--- a/tests/syntax/static_formals_1.c
+++ b/tests/syntax/static_formals_1.c
@@ -1,7 +1,6 @@
/* run.config
STDOPT: +"@PTEST_DIR@/static_formals_2.c" +"-cpp-extra-args=\"-I @PTEST_DIR@\"" +"-kernel-msg-key printer:vid"
*/
-
#include "static_formals.h"
int g() { return f(4); }
diff --git a/tests/syntax/string_concat.c b/tests/syntax/string_concat.c
index 924e8b423c7f30720939ddfb15b23b5c78ddc01b..b78a7d85590f3c5981b36737e9d20ec207dc0aad 100644
--- a/tests/syntax/string_concat.c
+++ b/tests/syntax/string_concat.c
@@ -1,4 +1,5 @@
/* run.config*
+PLUGIN: eva,scope variadic
TIMEOUT: 600
OPT: -eva
*/
diff --git a/tests/syntax/test_config b/tests/syntax/test_config
index df749c62084f1dff34265d08aa76546e4a89949e..3d75cb1ea823f0885cd7c5d9e4be187df1b0b67d 100644
--- a/tests/syntax/test_config
+++ b/tests/syntax/test_config
@@ -1,4 +1,5 @@
COMMENT: this directory is meant to test exclusively the front-end
COMMENT: (parser, type-checker, linker, syntactic transformations)
-OPT: -print -journal-disable -check -machdep x86_32
+PLUGIN:
+OPT: -print -machdep x86_32
FILEREG:.*\.\(c\|i\|ci\)$
diff --git a/tests/syntax/unroll_labels.i b/tests/syntax/unroll_labels.i
index 66da8b7cf4882b0214a9cc46294e20ff7f81668b..4fcef3f5d46dfd9784cf49c16fa8fbe38b7c99f4 100644
--- a/tests/syntax/unroll_labels.i
+++ b/tests/syntax/unroll_labels.i
@@ -1,10 +1,10 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-eva @EVA_CONFIG@"
STDOPT: +"-eva @EVA_CONFIG@ -main main2 -eva-slevel 3"
*/
enum { SIX = 6 } ;
volatile foo;
-
void main () {
int j = 0;
/*@ loop pragma UNROLL "completely", 4; */
diff --git a/tests/syntax/unroll_property_status_bts1442.i b/tests/syntax/unroll_property_status_bts1442.i
index 70ac3a9bbafb983c076f2aa1f3b6960753d24444..0a8970b5b8990d77268c0b7a7e2b8d8f54512e28 100644
--- a/tests/syntax/unroll_property_status_bts1442.i
+++ b/tests/syntax/unroll_property_status_bts1442.i
@@ -1,8 +1,8 @@
/* run.config
-OPT: -report
-OPT: -ulevel -1 -report
+PLUGIN: report
+ OPT: -report
+ OPT: -ulevel -1 -report
*/
-
int u(void);
char *strcpy(char*dst, char*src) {
diff --git a/tests/syntax/unroll_visit.i b/tests/syntax/unroll_visit.i
index 495b3bd0c50ce064137350a98b95406b6d5ed3ff..f4d949c53ef9a94e93a366b61bbb2a14caf8356c 100644
--- a/tests/syntax/unroll_visit.i
+++ b/tests/syntax/unroll_visit.i
@@ -1,7 +1,10 @@
/* run.config
+PLUGIN: eva,scope,from,inout
STDOPT: +"-eva @EVA_CONFIG@ -deps -out -input -deps"
*/
+
typedef char i8; // ideally, pretty-printing should keep 'i8' for some casts
+
void main() {
/*@ loop pragma UNROLL 2; */
for(i8 i=0; i<100; i++) {
diff --git a/tests/syntax/variadic.i b/tests/syntax/variadic.i
index b07b22acab044134cb870e6860a21a96783784ab..fc23e732c0c17b9d7407c4a07236490a6a0dc62d 100644
--- a/tests/syntax/variadic.i
+++ b/tests/syntax/variadic.i
@@ -1,8 +1,14 @@
+/* run.config
+ PLUGIN: variadic
+ STDOPT:
+*/
int normal(int n);
int vf(int x, ...);
+
typedef char tt;
struct T {int a;} st;
+
tt abstract;
unsigned char uchar;
signed char chr;
@@ -14,7 +20,7 @@ double d;
void h();
void g() {
- vf(1,1u,uchar,3.0f, ushort, ll, abstract, st, ld,d);
+ vf(1,1u,uchar,3.0f, ushort, ll, abstract, st, ld,d);
// vf() is variadic: the default argument promotions apply after the initial
// arguments. C99 6.5.2.2:7
f(1,uchar); // f undeclared, default argument promotions apply C99 6.5.2.2:6
diff --git a/tests/syntax/wstring_concat.c b/tests/syntax/wstring_concat.c
index 76f68ddd1b187f24f22591786cda9f13ce1a8209..9bd6571dd63b901380598f6dc29c9b769f8f6f24 100644
--- a/tests/syntax/wstring_concat.c
+++ b/tests/syntax/wstring_concat.c
@@ -1,8 +1,8 @@
/* run.config*
+PLUGIN: eva,scope,variadic
TIMEOUT: 600
OPT: -eva
*/
-
#include <wchar.h>
#include <stdio.h>
diff --git a/tests/test_config b/tests/test_config
index 11d75bf850c7c2f65ff98bf5fd486ec47200f499..f188ff4072509a1f23ce78441acaac71a8d02cf9 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,3 +1,6 @@
+MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
-OPT: -eva @EVA_CONFIG@ -journal-disable -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 ff3a028903375e622d271ae85a070bdad02df8cb..411673ceafcafde7b9e20b8a40abe841a1cbd1a5 100644
--- a/tests/test_config_apron
+++ b/tests/test_config_apron
@@ -1,7 +1,9 @@
+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@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
# Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_equality b/tests/test_config_equality
index ffa23c9d32dac550f13db32f54185a48c1b3772e..fff8c6fb43f010c4d22835dbf0a4e5c43f2a249f 100644
--- a/tests/test_config_equality
+++ b/tests/test_config_equality
@@ -1,7 +1,9 @@
+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@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
# Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_gauges b/tests/test_config_gauges
index 2c04eba2c74acdaa705e8dc6437b577266183d32..37ea7dfeb18c677bbb3d58d199a4d7030cd5dcac 100644
--- a/tests/test_config_gauges
+++ b/tests/test_config_gauges
@@ -1,7 +1,9 @@
+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
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
# Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_octagon b/tests/test_config_octagon
index c3f170e9652940aae572fa469a014cb5da8baf23..a63c091418a391a00eee6a9f0bb681358a49d7c5 100644
--- a/tests/test_config_octagon
+++ b/tests/test_config_octagon
@@ -1,7 +1,9 @@
+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@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
# Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index d25a43c5eb7a0aeff3b6cddcdda469a1433ba638..3b082f3869cd61f8bb7baf1944ea34ca3eb2e66f 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -1,7 +1,9 @@
+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@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
# Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps