diff --git a/src/plugins/wp/.gitignore b/src/plugins/wp/.gitignore
index baf16ae83ffec9265fefa372a36536575bc15b60..6f6f4289b01e7f2d93bc1e30518c98846c37b47a 100644
--- a/src/plugins/wp/.gitignore
+++ b/src/plugins/wp/.gitignore
@@ -9,6 +9,7 @@
/tests/*/oracle/dune
+/tests/*/oracle_*/dune
/tests/*/result
/tests/*/result_*
/tests/*/*.sav
diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config
index af58095c66525f1e8d0f737cfb43a205463f9f1d..a44281d72b1b95c191aebf7a7663ad268aa72f51 100644
--- a/src/plugins/wp/tests/test_config
+++ b/src/plugins/wp/tests/test_config
@@ -1,3 +1,3 @@
-PLUGIN: wp,rtegen
+PLUGIN: rtegen,wp
CMD: @frama-c@ -wp -wp-prover none -wp-print -wp-share ../../../share -wp-msg-key shell
OPT:
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 6883d9ff47b14241d62896e3a1b147d82aa80ba1..3ee3adf57160622eb7c20ff61159eab539887f08 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,3 +1,4 @@
-PLUGIN: wp,rtegen
-CMD: @frama-c@ -wp -wp-par 1 -wp-share ../../../share -wp-msg-key shell -wp-report %{dep:../../qualif.report} -wp-session @PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay -wp-coq-timeout 120
+PLUGIN: rtegen,wp
+MACRO: WP_OPTIONS -wp -wp-par 1 -wp-share ../../../share -wp-msg-key shell -wp-report %{dep:../../qualif.report} -wp-session @PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay -wp-coq-timeout 120
+CMD: @frama-c@ @WP_OPTIONS@
OPT:
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
index b206efad0519db1f347ae4a6b79e5221ff611f9d..698d8db712256e9a0b1573f5bc7c813aeb70b520 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
@@ -1,7 +1,7 @@
/* run.config_qualif
- OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key shell
+ MODULE: stmtcompiler_test_rela.cmxs
+ OPT: -wp-msg-key shell
*/
-
int empty (int c){
c = c < 0 ? c + 10 : c+100;
int tmp;
diff --git a/src/plugins/wp/tests/wp/wp_strategy.c b/src/plugins/wp/tests/wp/wp_strategy.c
index c514347a72a233922e656c26095d63647feea376..9910f3140a430e342bdfd24df6cc4a23ebd7c1d7 100644
--- a/src/plugins/wp/tests/wp/wp_strategy.c
+++ b/src/plugins/wp/tests/wp/wp_strategy.c
@@ -1,10 +1,10 @@
/* run.config
-OPT: -journal-disable -wp-model Hoare -wp-verbose 2
-OPT: -journal-disable -wp-model Typed -wp-verbose 2 -wp-prop @assigns
+OPT: -wp-model Hoare -wp-verbose 2
+OPT: -wp-model Typed -wp-verbose 2 -wp-prop @assigns
*/
/* run.config_qualif
-OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key shell
+OPT: -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key shell
*/
/*----------------------------------------------------------------------------*/
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
index 0fabb9c099152b4e092f96eb5bf0d1c504c7b96d..18083135d8fdbf9772d7e9c0805bfb74a2794dda 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
@@ -5,32 +5,23 @@
[wp] logic.i:65: Warning:
Cast with incompatible pointers types (source: __anonstruct_Buint_4*)
(target: uint32*)
-[wp] logic.i:49: Warning:
- Logic cast from struct (Tint2) not implemented yet
-[wp] logic.i:50: Warning:
- Logic cast from struct (Point) not implemented yet
+[wp] logic.i:49: Warning: Logic cast from struct (Tint2) not implemented yet
+[wp] logic.i:50: Warning: Logic cast from struct (Point) not implemented yet
[wp] logic.i:51: Warning:
Logic cast to struct (Point) from (int [2]) not implemented yet
-[wp] logic.i:52: Warning:
- Logic cast from struct (Point) not implemented yet
-[wp] logic.i:53: Warning:
- Logic cast from struct (Tint2) not implemented yet
-[wp] logic.i:54: Warning:
- Logic cast from struct (Buint) not implemented yet
+[wp] logic.i:52: Warning: Logic cast from struct (Point) not implemented yet
+[wp] logic.i:53: Warning: Logic cast from struct (Tint2) not implemented yet
+[wp] logic.i:54: Warning: Logic cast from struct (Buint) not implemented yet
[wp] logic.i:55: Warning:
Logic cast to struct (Buint) from (unsigned int) not implemented yet
-[wp] logic.i:56: Warning:
- Logic cast from struct (Tint6) not implemented yet
+[wp] logic.i:56: Warning: Logic cast from struct (Tint6) not implemented yet
[wp] logic.i:57: Warning:
Logic cast to sized array (Triangle) from (int [6]) not implemented yet
-[wp] logic.i:58: Warning:
- Logic cast from struct (Tint6) not implemented yet
-[wp] logic.i:59: Warning:
- Logic cast from struct (Tint6) not implemented yet
+[wp] logic.i:58: Warning: Logic cast from struct (Tint6) not implemented yet
+[wp] logic.i:59: Warning: Logic cast from struct (Tint6) not implemented yet
[wp] logic.i:60: Warning:
Logic cast to sized array (int [2]) from (int [6]) not implemented yet
-[wp] logic.i:61: Warning:
- Logic cast from struct (Tint6) not implemented yet
+[wp] logic.i:61: Warning: Logic cast from struct (Tint6) not implemented yet
[wp] logic.i:62: Warning:
Logic cast to struct (Tint2) from (int [6]) not implemented yet
[wp] 21 goals scheduled
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
index 2e058d9e213b9fbb7f9a383b49cbd192d627a512..7b8caf21e8e377e7978fa309d5516fa51ecd1a43 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
@@ -2,10 +2,8 @@
[kernel] Parsing pointer.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] pointer.i:50: Warning:
- Uncomparable locations p_0 and mem:t.(0)
-[wp] pointer.i:49: Warning:
- Uncomparable locations p_0 and mem:t.(0)
+[wp] pointer.i:50: Warning: Uncomparable locations p_0 and mem:t.(0)
+[wp] pointer.i:49: Warning: Uncomparable locations p_0 and mem:t.(0)
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_ref_array_ensures_Lt : Valid
[wp] [Qed] Goal typed_ref_array_ensures_Le : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
index ac454864f98e4bfaae0ae87e2d0ded1f71f30a0f..89230ae3df2decde5a66b784944b066430bc3fbc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
@@ -2,10 +2,8 @@
[kernel] Parsing pointer.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] pointer.i:50: Warning:
- Uncomparable locations p_0 and mem:t.(0)
-[wp] pointer.i:49: Warning:
- Uncomparable locations p_0 and mem:t.(0)
+[wp] pointer.i:50: Warning: Uncomparable locations p_0 and mem:t.(0)
+[wp] pointer.i:49: Warning: Uncomparable locations p_0 and mem:t.(0)
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_array_ensures_Lt : Valid
[wp] [Qed] Goal typed_array_ensures_Le : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle
index 7fcb2ffab9dd9e54cbf13724180b80c5c625cfa6..5f9156c6e2e5a897b546fa4cd55867e9693a767e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle
@@ -1,37 +1,21 @@
# frama-c -wp [...]
[kernel] Parsing precedence.i (no preprocessing)
-[kernel:annot-error] precedence.i:90: Warning:
- unexpected token ';'
-[kernel:annot-error] precedence.i:135: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:134: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:133: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:132: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:130: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:129: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:128: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:127: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:125: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:124: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:123: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:122: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:120: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:119: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:118: Warning:
- Inconsistent relation chain.
+[kernel:annot-error] precedence.i:90: Warning: unexpected token ';'
+[kernel:annot-error] precedence.i:135: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:134: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:133: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:132: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:130: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:129: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:128: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:127: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:125: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:124: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:123: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:122: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:120: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:119: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:118: Warning: Inconsistent relation chain.
[kernel:annot-error] precedence.i:175: Warning:
R is not a logic variable. Ignoring code annotation
[kernel:annot-error] precedence.i:176: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
index d08db8de9fe6ddc3efa9ff9365897e40ce0ab081..16e3d0be1361b913238cfbae5c6db15a2b599285 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
@@ -1,37 +1,21 @@
# frama-c -wp -wp-steps 50 [...]
[kernel] Parsing precedence.i (no preprocessing)
-[kernel:annot-error] precedence.i:90: Warning:
- unexpected token ';'
-[kernel:annot-error] precedence.i:135: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:134: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:133: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:132: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:130: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:129: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:128: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:127: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:125: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:124: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:123: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:122: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:120: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:119: Warning:
- Inconsistent relation chain.
-[kernel:annot-error] precedence.i:118: Warning:
- Inconsistent relation chain.
+[kernel:annot-error] precedence.i:90: Warning: unexpected token ';'
+[kernel:annot-error] precedence.i:135: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:134: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:133: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:132: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:130: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:129: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:128: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:127: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:125: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:124: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:123: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:122: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:120: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:119: Warning: Inconsistent relation chain.
+[kernel:annot-error] precedence.i:118: Warning: Inconsistent relation chain.
[kernel:annot-error] precedence.i:175: Warning:
R is not a logic variable. Ignoring code annotation
[kernel:annot-error] precedence.i:176: Warning:
diff --git a/src/plugins/wp/tests/wp_bts/issue_143.i b/src/plugins/wp/tests/wp_bts/issue_143.i
index 555cbcb5b0889741e7ebe50de2d0713662fb9934..0c8b29cae6acc3d145373ca1d735c9f579f5559c 100644
--- a/src/plugins/wp/tests/wp_bts/issue_143.i
+++ b/src/plugins/wp/tests/wp_bts/issue_143.i
@@ -2,11 +2,11 @@
DONTRUN:
*/
/* run.config_qualif
- EXECNOW: chmod a-x ./tests/inexistant-prover
+ CMD: chmod a-x %{dep:../../inexistant-prover} && @frama-c@ @WP_OPTIONS@
OPT: -wp
- OPT: -wp -wp-prover "alt-ergo,native:coq" -wp-alt-ergo ./tests/inexistant-prover -wp-coqc ./tests/inexistant-prover
- OPT: -wp -wp-prover "alt-ergo" -wp-alt-ergo ./tests/inexistant-prover
- OPT: -wp -wp-prover "native:coq" -wp-coqc ./tests/inexistant-prover
+ OPT: -wp -wp-prover "alt-ergo,native:coq" -wp-alt-ergo %{dep:../../inexistant-prover} -wp-coqc %{dep:../../inexistant-prover}
+ OPT: -wp -wp-prover "alt-ergo" -wp-alt-ergo %{dep:../../inexistant-prover}
+ OPT: -wp -wp-prover "native:coq" -wp-coqc %{dep:../../inexistant-prover}
*/
/*@
diff --git a/src/plugins/wp/tests/wp_plugin/config.i b/src/plugins/wp/tests/wp_plugin/config.i
index 3653e881697196e82af4a05196d923fc730c67e0..8f0f0e9a526ce2621b1b7442b38d0e9c76e26aa0 100644
--- a/src/plugins/wp/tests/wp_plugin/config.i
+++ b/src/plugins/wp/tests/wp_plugin/config.i
@@ -1,8 +1,8 @@
/* run.config
DONTRUN:
*/
-
/* run.config_qualif
- CMD: tests/wp_plugin/config.sh
+ DEPS: config.sh
+ CMD: config.sh
OPT:
*/
diff --git a/src/plugins/wp/tests/wp_plugin/convert.i b/src/plugins/wp/tests/wp_plugin/convert.i
index 630c406f9676e288b6fedf7f56b5bd86006d5d1b..2c16c20f5c84acc15e9d6da9feadaeb2e8e69633 100644
--- a/src/plugins/wp/tests/wp_plugin/convert.i
+++ b/src/plugins/wp/tests/wp_plugin/convert.i
@@ -4,7 +4,7 @@
/* run.config_qualif
OPT:
- OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report
+ OPT: -wp-prover native:alt-ergo -wp-report=%{dep:../../native.report}
*/
// --------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/doomed_report_ko.i b/src/plugins/wp/tests/wp_plugin/doomed_report_ko.i
index 2189024b22ebf9d8292cfcc6b9aa7d7a6c7a9af6..3dbf363410d4c03d92c0da57a316b1149ccc8fed 100644
--- a/src/plugins/wp/tests/wp_plugin/doomed_report_ko.i
+++ b/src/plugins/wp/tests/wp_plugin/doomed_report_ko.i
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- OPT: -wp-smoke-tests -wp-report tests/wp_plugin/doomed.report
+ OPT: -wp-smoke-tests -wp-report %{dep:doomed.report}
*/
/*@ axiomatic CFG {
diff --git a/src/plugins/wp/tests/wp_plugin/doomed_report_ok.i b/src/plugins/wp/tests/wp_plugin/doomed_report_ok.i
index 1b4f94519a27476677b15fee36c129bf4eb61e9a..28e59c7a9b7dab3ea2ad33d53850805013f0802d 100644
--- a/src/plugins/wp/tests/wp_plugin/doomed_report_ok.i
+++ b/src/plugins/wp/tests/wp_plugin/doomed_report_ok.i
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- OPT: -wp-smoke-tests -wp-report tests/wp_plugin/doomed.report
+ OPT: -wp-smoke-tests -wp-report %{dep:doomed.report}
*/
/*@ axiomatic CFG {
diff --git a/src/plugins/wp/tests/wp_plugin/math.i b/src/plugins/wp/tests/wp_plugin/math.i
index 160d94e7bee83c4caeeff4227a9a579d10c923a9..fb2e979b8ac00bc40a5c979eeb37004343c1ed46 100644
--- a/src/plugins/wp/tests/wp_plugin/math.i
+++ b/src/plugins/wp/tests/wp_plugin/math.i
@@ -3,10 +3,10 @@
*/
/* run.config_qualif
- OPT: -wp-prover alt-ergo -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
- OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
- OPT: -wp-prover alt-ergo -wp-prop=ko -wp-timeout 100 -wp-steps 10
- OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=ko -wp-timeout 100 -wp-steps 10
+ OPT: -wp-prover alt-ergo -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
+ OPT: -wp-prover native:alt-ergo -wp-report=%{dep:../../native.report} -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
+ OPT: -wp-prover alt-ergo -wp-prop=ko -wp-timeout 100 -wp-steps 10
+ OPT: -wp-prover native:alt-ergo -wp-report=%{dep:../../native.report} -wp-prop=ko -wp-timeout 100 -wp-steps 10
*/
// --------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/no_step_limit.i b/src/plugins/wp/tests/wp_plugin/no_step_limit.i
index d1ad1d007aab8783123f81c1e3e37e9480154377..aa14e395d954c821ecc1ffb800781552f4f3fb3e 100644
--- a/src/plugins/wp/tests/wp_plugin/no_step_limit.i
+++ b/src/plugins/wp/tests/wp_plugin/no_step_limit.i
@@ -2,7 +2,7 @@
DONTRUN:
*/
/* run.config_qualif
- CMD: WHY3CONFIG=@PTEST_DIR@/@PTEST_NAME@.conf @frama-c@
+ CMD: WHY3CONFIG=@PTEST_NAME@.conf @frama-c@
OPT: -wp -wp-prover no-steps -wp-steps 10 -wp-timeout 1 -wp-cache none -wp-no-cache-env -wp-msg-key shell
*/
// cache is locally deactivated to see the option
diff --git a/src/plugins/wp/tests/wp_plugin/nosession.i b/src/plugins/wp/tests/wp_plugin/nosession.i
index 36b69197ada328bde3c048c4d8e4d5ad31ba4125..28e1622720c2aa7f47e4b9df1e149a4be4c4e57e 100644
--- a/src/plugins/wp/tests/wp_plugin/nosession.i
+++ b/src/plugins/wp/tests/wp_plugin/nosession.i
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp-share ../../../share -wp-msg-key shell
+ CMD: @frama-c@ -wp-share ../../../share -wp-msg-key shell
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/oracle_qualif/removed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
index c961a5d468de1dc6bdf09be57972f87aef6dd2e0..b6f0a74d7aa8d0e02e8c0c967a295a4a41969734 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
@@ -5,8 +5,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] removed.i:9: Warning:
- signed overflow. assert 1 + i ≤ 2147483647;
+[eva:alarm] removed.i:10: Warning: signed overflow. assert 1 + i ≤ 2147483647;
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
index 5fa488ad8824c3a4945959941a8b5d198c3995c1..9efba93bde83103ce06ccbb72bb4a49d1d0b2276 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
@@ -2,8 +2,7 @@
[kernel] Parsing repeat.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] repeat.c:47: Warning:
- Missing assigns clause (assigns 'everything' instead)
+[wp] repeat.c:47: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] 47 goals scheduled
[wp] [Qed] Goal typed_master_ensures : Valid
[wp] [Qed] Goal typed_master_assigns_exit : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
index 583f4d36f0886bdb9e400a01be8bc0d7723ec389..54cef061daae82165164b4e9b0aba11cf276822f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
@@ -1,5 +1,5 @@
# frama-c -wp -wp-model 'Dump' [...]
-[kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
+[kernel] Parsing stmt.c (with preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal f_exits : Valid (Unreachable)
[wp] [CFG] Goal g_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index 9a4824f460e97fc22bacd03aae895c0e4c6147eb..97897910e2ce91d4e539e5a0f1ed75f5d96907cb 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,5 +1,6 @@
/* 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: @PLUGIN@ from,inout,eva,scope
+ OPT: -no-wp -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
*/
/* run.config
diff --git a/src/plugins/wp/tests/wp_plugin/stmt.c b/src/plugins/wp/tests/wp_plugin/stmt.c
index 58e04b9d85fccbba9f6eb09c1738dffc0c98768c..203ee97d9d2975c44ca56d1b2a87699f4c16ae03 100644
--- a/src/plugins/wp/tests/wp_plugin/stmt.c
+++ b/src/plugins/wp/tests/wp_plugin/stmt.c
@@ -1,12 +1,12 @@
/* run.config
- OPT: -load-module report -then -report
+ PLUGIN: @PLUGIN@ report
+ OPT: -then -report
*/
-
/* run.config_qualif
- OPT: -load-module report -then -report
- EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
+ PLUGIN: @PLUGIN@ report
+ OPT: -then -report
+ EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -wp-precond-weakening -wp -wp-model Dump -wp-out . -wp-msg-key shell 1> stmt.log
*/
-
/*@ ensures a > 0 ==> \result == a + b;
@ ensures a <= 0 ==> \result == -1;
*/
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
index 7d6f12f66d12dcc3006b3c17fb5bc2a54bbc3c66..4b78ecb6f3cbaebc7da8e26e620fe4168389947d 100644
--- a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
+++ b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
@@ -1,9 +1,9 @@
/* run.config
OPT: -wp -wp-prover none
*/
-
/* run.config_qualif
- OPT: -load-module tests/wp_tip/TacNOP.ml -wp -wp-par 1 -wp-prover script
+ MODULE: TacNOP.cmxs
+ OPT: -wp -wp-par 1 -wp-prover script
*/
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle
index f75ed8ad5fe7f376c80b34b30de474e1ba62e951..65ff9d0005cd3cb565634d614bf84a3a3f0d489e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing array_initialized.c (with preprocessing)
-[kernel] array_initialized.c:13: Warning:
- Too many initializers for array g
+[kernel] array_initialized.c:13: Warning: Too many initializers for array g
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle
index f75ed8ad5fe7f376c80b34b30de474e1ba62e951..65ff9d0005cd3cb565634d614bf84a3a3f0d489e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing array_initialized.c (with preprocessing)
-[kernel] array_initialized.c:13: Warning:
- Too many initializers for array g
+[kernel] array_initialized.c:13: Warning: Too many initializers for array g
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled