From ee81a72587e0bd57a5e686577d325ba1de8d323e Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 20 Oct 2020 11:14:17 +0200
Subject: [PATCH] [Tests] add test config qualif of wp (cont.)
---
src/plugins/wp/.gitignore | 1 +
src/plugins/wp/tests/test_config | 2 +-
src/plugins/wp/tests/test_config_qualif | 5 +-
.../wp/tests/wp/stmtcompiler_test_rela.i | 4 +-
src/plugins/wp/tests/wp/wp_strategy.c | 6 +--
.../wp_acsl/oracle_qualif/logic.res.oracle | 27 ++++-------
.../oracle_qualif/pointer.0.res.oracle | 6 +--
.../oracle_qualif/pointer.1.res.oracle | 6 +--
.../oracle_qualif/precedence.0.res.oracle | 48 +++++++------------
.../oracle_qualif/precedence.1.res.oracle | 48 +++++++------------
src/plugins/wp/tests/wp_bts/issue_143.i | 8 ++--
src/plugins/wp/tests/wp_plugin/config.i | 4 +-
src/plugins/wp/tests/wp_plugin/convert.i | 2 +-
.../wp/tests/wp_plugin/doomed_report_ko.i | 2 +-
.../wp/tests/wp_plugin/doomed_report_ok.i | 2 +-
src/plugins/wp/tests/wp_plugin/math.i | 8 ++--
.../wp/tests/wp_plugin/no_step_limit.i | 2 +-
src/plugins/wp/tests/wp_plugin/nosession.i | 2 +-
.../oracle_qualif/removed.res.oracle | 3 +-
.../wp_plugin/oracle_qualif/repeat.res.oracle | 3 +-
.../wp/tests/wp_plugin/oracle_qualif/stmt.log | 2 +-
src/plugins/wp/tests/wp_plugin/removed.i | 3 +-
src/plugins/wp/tests/wp_plugin/stmt.c | 10 ++--
.../wp/tests/wp_tip/tac_split_quantifiers.i | 4 +-
.../array_initialized.0.res.oracle | 3 +-
.../array_initialized.1.res.oracle | 3 +-
26 files changed, 84 insertions(+), 130 deletions(-)
diff --git a/src/plugins/wp/.gitignore b/src/plugins/wp/.gitignore
index baf16ae83ff..6f6f4289b01 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 af58095c665..a44281d72b1 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 6883d9ff47b..3ee3adf5716 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 b206efad051..698d8db7122 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 c514347a72a..9910f3140a4 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 0fabb9c0991..18083135d8f 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 2e058d9e213..7b8caf21e8e 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 ac454864f98..89230ae3df2 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 7fcb2ffab9d..5f9156c6e2e 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 d08db8de9fe..16e3d0be136 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 555cbcb5b08..0c8b29cae6a 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 3653e881697..8f0f0e9a526 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 630c406f967..2c16c20f5c8 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 2189024b22e..3dbf363410d 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 1b4f94519a2..28e59c7a9b7 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 160d94e7bee..fb2e979b8ac 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 d1ad1d007aa..aa14e395d95 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 36b69197ada..28e1622720c 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 c961a5d468d..b6f0a74d7aa 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 5fa488ad882..9efba93bde8 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 583f4d36f08..54cef061daa 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 9a4824f460e..97897910e2c 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 58e04b9d85f..203ee97d9d2 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 7d6f12f66d1..4b78ecb6f3c 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 f75ed8ad5fe..65ff9d0005c 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 f75ed8ad5fe..65ff9d0005c 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
--
GitLab