From 7b818ee49b86fbada8aa3bac0ef348adb0bce74c Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 24 Jan 2024 09:34:07 +0100
Subject: [PATCH] [wp] dedicated dir/config for CE tests
---
src/plugins/wp/tests/ptests_config | 4 +++-
src/plugins/wp/tests/{wp_plugin => wp_ce}/cvc4_ce.i | 8 ++++++--
.../tests/{wp_plugin => wp_ce}/oracle/cvc4_ce.res.oracle | 2 +-
.../tests/{wp_plugin => wp_ce}/oracle/probes.res.oracle | 8 ++++----
.../oracle_qualif => wp_ce/oracle_ce}/cvc4_ce.res.oracle | 6 +++---
src/plugins/wp/tests/{wp_plugin => wp_ce}/probes.i | 5 ++++-
src/plugins/wp/tests/wp_ce/test_config_ce | 3 +++
7 files changed, 24 insertions(+), 12 deletions(-)
rename src/plugins/wp/tests/{wp_plugin => wp_ce}/cvc4_ce.i (85%)
rename src/plugins/wp/tests/{wp_plugin => wp_ce}/oracle/cvc4_ce.res.oracle (93%)
rename src/plugins/wp/tests/{wp_plugin => wp_ce}/oracle/probes.res.oracle (92%)
rename src/plugins/wp/tests/{wp_plugin/oracle_qualif => wp_ce/oracle_ce}/cvc4_ce.res.oracle (88%)
rename src/plugins/wp/tests/{wp_plugin => wp_ce}/probes.i (91%)
create mode 100644 src/plugins/wp/tests/wp_ce/test_config_ce
diff --git a/src/plugins/wp/tests/ptests_config b/src/plugins/wp/tests/ptests_config
index d53499bf328..5221e8c0f16 100644
--- a/src/plugins/wp/tests/ptests_config
+++ b/src/plugins/wp/tests/ptests_config
@@ -1,6 +1,8 @@
-DEFAULT_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
+DEFAULT_SUITES= wp wp_acsl wp_plugin wp_ce wp_bts wp_store wp_hoare
DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip
qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip
qualif_SUITES= why3
+
+ce_SUITES= wp_ce
diff --git a/src/plugins/wp/tests/wp_plugin/cvc4_ce.i b/src/plugins/wp/tests/wp_ce/cvc4_ce.i
similarity index 85%
rename from src/plugins/wp/tests/wp_plugin/cvc4_ce.i
rename to src/plugins/wp/tests/wp_ce/cvc4_ce.i
index 853f90943c0..cff74da54d7 100644
--- a/src/plugins/wp/tests/wp_plugin/cvc4_ce.i
+++ b/src/plugins/wp/tests/wp_ce/cvc4_ce.i
@@ -1,6 +1,10 @@
-/* run.config_qualif
+/* run.config_ce
OPT: -wp -wp-counter-examples -wp-prover cvc4 -wp-status
- */
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
//@ check lemma wrong: \forall integer x; \abs(x) == x;
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cvc4_ce.res.oracle b/src/plugins/wp/tests/wp_ce/oracle/cvc4_ce.res.oracle
similarity index 93%
rename from src/plugins/wp/tests/wp_plugin/oracle/cvc4_ce.res.oracle
rename to src/plugins/wp/tests/wp_ce/oracle/cvc4_ce.res.oracle
index 2832c47376f..c98d32bed6c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cvc4_ce.res.oracle
+++ b/src/plugins/wp/tests/wp_ce/oracle/cvc4_ce.res.oracle
@@ -16,7 +16,7 @@ Prove: IAbs.abs(x) = x.
Function wrong
------------------------------------------------------------
-Goal Post-condition (file cvc4_ce.i, line 7) in 'wrong':
+Goal Post-condition (file cvc4_ce.i, line 11) in 'wrong':
Assume { Type: is_sint32(wrong_0). }
Prove: IAbs.abs(wrong_0) = wrong_0.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/probes.res.oracle b/src/plugins/wp/tests/wp_ce/oracle/probes.res.oracle
similarity index 92%
rename from src/plugins/wp/tests/wp_plugin/oracle/probes.res.oracle
rename to src/plugins/wp/tests/wp_ce/oracle/probes.res.oracle
index 3d6665bc5c4..cc0cb7183aa 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/probes.res.oracle
+++ b/src/plugins/wp/tests/wp_ce/oracle/probes.res.oracle
@@ -8,7 +8,7 @@
Function get
------------------------------------------------------------
-Goal Post-condition (file probes.i, line 9) in 'get':
+Goal Post-condition (file probes.i, line 12) in 'get':
Let x = -i_2.
Assume {
Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\
@@ -32,19 +32,19 @@ Prove: false.
------------------------------------------------------------
Goal Assigns nothing in 'get' (1/3):
-Effect at line 13
+Effect at line 16
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'get' (2/3):
-Effect at line 15
+Effect at line 18
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'get' (3/3):
-Effect at line 17
+Effect at line 20
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/cvc4_ce.res.oracle b/src/plugins/wp/tests/wp_ce/oracle_ce/cvc4_ce.res.oracle
similarity index 88%
rename from src/plugins/wp/tests/wp_plugin/oracle_qualif/cvc4_ce.res.oracle
rename to src/plugins/wp/tests/wp_ce/oracle_ce/cvc4_ce.res.oracle
index ca0d3106e81..ab352704f50 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/cvc4_ce.res.oracle
+++ b/src/plugins/wp/tests/wp_ce/oracle_ce/cvc4_ce.res.oracle
@@ -5,8 +5,8 @@
[wp] [Valid] Goal wrong_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
-[wp] [Unsuccess] typed_check_lemma_wrong (CVC4) (No Cache) (Model)
-[wp] [Unsuccess] typed_wrong_ensures (CVC4) (No Cache) (Model)
+[wp] [Unsuccess] typed_check_lemma_wrong (CVC4) (Model)
+[wp] [Unsuccess] typed_wrong_ensures (CVC4) (Model)
[wp] [Valid] typed_wrong_assigns (Qed)
[wp] Proved goals: 3 / 5
Terminating: 1
@@ -28,7 +28,7 @@ Model x = -1
Function wrong
------------------------------------------------------------
-Goal Post-condition (file cvc4_ce.i, line 7) in 'wrong':
+Goal Post-condition (file cvc4_ce.i, line 11) in 'wrong':
Assume { Type: is_sint32(wrong_0). Probe x = wrong_0. }
Prove: IAbs.abs(wrong_0) = wrong_0.
Prover CVC4 returns Unsuccess (Model)
diff --git a/src/plugins/wp/tests/wp_plugin/probes.i b/src/plugins/wp/tests/wp_ce/probes.i
similarity index 91%
rename from src/plugins/wp/tests/wp_plugin/probes.i
rename to src/plugins/wp/tests/wp_ce/probes.i
index cc998c170c6..03ccb78a433 100644
--- a/src/plugins/wp/tests/wp_plugin/probes.i
+++ b/src/plugins/wp/tests/wp_ce/probes.i
@@ -1,6 +1,9 @@
/* run.config_qualif
DONTRUN:
- */
+*/
+/* run.config_ce
+ DONTRUN:
+*/
// Matrix addessing
diff --git a/src/plugins/wp/tests/wp_ce/test_config_ce b/src/plugins/wp/tests/wp_ce/test_config_ce
new file mode 100644
index 00000000000..c3e8d3e1aaf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_ce/test_config_ce
@@ -0,0 +1,3 @@
+PLUGIN: wp
+CMD: @frama-c@ -wp -wp-par 1 -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-cache none
+OPT:
--
GitLab