From b003e55fc72a97f4c956b76b7ee5581f4d26defe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 2 Sep 2024 13:17:29 +0200
Subject: [PATCH] [wp] updated oracles & scripts
---
src/plugins/wp/tests/why3/test_config_qualif | 2 +-
.../script/lemma_res_n.json | 9 +++----
.../script/lemma_res_y.json | 9 +++----
.../wp_plugin/oracle_qualif/config.res.oracle | 4 +--
.../oracle_qualif/fallback.res.oracle | 2 +-
.../oracle_qualif/unsigned.res.oracle | 8 +++---
.../script/lemma_U32.json | 27 ++++++++++++++++---
.../script/lemma_ByInd.json | 19 +++++++------
.../script/lemma_ByInd.json | 15 +++++------
.../script/lemma_ByInd.json | 15 +++++------
.../script/lemma_j_incr_char.json | 21 +++++++--------
.../script/lemma_j_incr_short.json | 21 +++++++--------
12 files changed, 82 insertions(+), 70 deletions(-)
diff --git a/src/plugins/wp/tests/why3/test_config_qualif b/src/plugins/wp/tests/why3/test_config_qualif
index 20cc9405105..d460c393a38 100644
--- a/src/plugins/wp/tests/why3/test_config_qualif
+++ b/src/plugins/wp/tests/why3/test_config_qualif
@@ -1,6 +1,6 @@
FILEREG: .*\.why
DEPS: ~/.why3.conf
-CMD: why3 -L @PTEST_SHARE_DIR@/why3 prove -P Alt-Ergo,2.5.3
+CMD: why3 -L @PTEST_SHARE_DIR@/why3 prove -P Alt-Ergo,2.5.4
OPT:
COMMENT: the filter remove the information about time and steps
FILTER: sed -e 's|\(.*\)\( (.*)\)|\1|'
diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json
index 354ccb74d22..00fcc7e2ae2 100644
--- a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json
+++ b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json
@@ -1,9 +1,8 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.0204 },
- { "header": "Bit-Test Range", "tactic": "Wp.bittestrange", "params": {},
+[ { "header": "Bit-Test Range", "tactic": "Wp.bittestrange", "params": {},
"select": { "select": "inside-step", "at": 1, "kind": "have", "occur": 0,
"target": "not (bit_test off_0 15)",
"pattern": "!bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "qed", "verdict": "valid" } ],
- "Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0204,
- "steps": 52 } ] } } ]
+ "Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.027549,
+ "steps": 38 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json
index 67707c14b56..ca56f4319e4 100644
--- a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json
+++ b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json
@@ -1,9 +1,8 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.0194 },
- { "header": "Bit-Test Range", "tactic": "Wp.bittestrange", "params": {},
+[ { "header": "Bit-Test Range", "tactic": "Wp.bittestrange", "params": {},
"select": { "select": "inside-step", "at": 1, "kind": "have", "occur": 0,
"target": "(bit_test off_0 15)",
"pattern": "bit_test$off15" },
- "children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0194,
- "steps": 52 } ],
+ "children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.021835,
+ "steps": 37 } ],
"Bit #15 (sup)": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
index 864714c2b18..00ab6f9978e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
@@ -1,8 +1,8 @@
----------------------------------------------------------
WP Requirements for Qualif Tests
----------------------------------------------------------
-1. The Alt-Ergo theorem prover, version v2.5.3
-2. The Why3 platform, version 1.7.1
+1. The Alt-Ergo theorem prover, version v2.5.4
+2. The Why3 platform, version 1.7.2
3. The environment variable FRAMAC_WP_CACHEDIR is defined
4. The environment variable FRAMAC_WP_CACHE is defined
----------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
index 6c923007a18..beee3d22091 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
@@ -5,7 +5,7 @@
[wp] [Valid] Goal job_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
-[wp] Warning: Prover Alt-Ergo:1.2.0 not found, fallback to Alt-Ergo:2.5.3
+[wp] Warning: Prover Alt-Ergo:1.2.0 not found, fallback to Alt-Ergo:2.5.4
[wp] [Valid] typed_job_ensures (Alt-Ergo) (Cached)
[wp] Proved goals: 3 / 3
Terminating: 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
index 234a6e8800c..f447a53a23f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
@@ -2,10 +2,10 @@
[kernel] Parsing unsigned.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] [Unsuccess] typed_lemma_U32 (Tactic) (Qed 1/2)
-[wp] Proved goals: 0 / 1
- Unsuccess: 1
+[wp] [Valid] typed_lemma_U32 (Tactics 3) (Qed 4/4)
+[wp] Proved goals: 1 / 1
+ Script: 1 (Tactics 3) (Qed 4/4)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Lemma - - 1 0.0%
+ Lemma - - 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json b/src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json
index 692d239230f..9aba6ba2c93 100644
--- a/src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json
+++ b/src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json
@@ -1,9 +1,28 @@
-[ { "prover": "script", "verdict": "unknown" },
- { "header": "Bitwise Eq.", "tactic": "Wp.bitwised",
+[ { "header": "Bitwise Eq.", "tactic": "Wp.bitwised",
"params": { "Wp.bitwised.range": 32 },
"select": { "select": "clause-goal",
"target": "(land 4294967295 x_0)=x_0",
"pattern": "=land$x4294967295$x" },
- "children": { "range": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ],
+ "children": { "range": [ { "header": "Split", "tactic": "Wp.split",
+ "params": {},
+ "select": { "select": "clause-goal",
+ "target": "(0<=x_0) /\\ (0<=(land 4294967295 x_0)) /\\ (x_0<=4294967295)",
+ "pattern": "&<=<=<=0$x0land$x42949672954294967295" },
+ "children": { "Goal 1/3": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Goal 2/3": [ { "header": "Bit Range",
+ "tactic": "Wp.bitrange",
+ "params":
+ { "positive-land": true,
+ "positive-lor": true },
+ "select":
+ { "select": "clause-goal",
+ "target": "0<=(land 4294967295 x_0)",
+ "pattern": "<=0land4294967295$x" },
+ "children":
+ { "bit-range":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 3/3": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json
index 41ee719bb82..18d14b4efae 100644
--- a/src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json
@@ -1,13 +1,12 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.04 },
- { "header": "Induction", "tactic": "Wp.induction",
+[ { "header": "Induction", "tactic": "Wp.induction",
"params": { "base": { "select": "kint", "val": "0" } },
"select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
"pattern": "L_f$x" },
- "children": { "Base": [ { "prover": "Alt-Ergo:2.5.3", "verdict": "valid",
- "time": 0.0035, "steps": 14 } ],
- "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0247,
- "steps": 325 } ],
- "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0118,
- "steps": 32 } ] } } ]
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.5.4", "verdict": "valid",
+ "time": 0.013909, "steps": 4 } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.02138,
+ "steps": 88 } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid",
+ "time": 0.026118, "steps": 116 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json
index c3ad89aead4..df8aacace3c 100644
--- a/src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json
@@ -1,11 +1,10 @@
-[ { "prover": "script", "verdict": "unknown" },
- { "header": "Induction", "tactic": "Wp.induction",
+[ { "header": "Induction", "tactic": "Wp.induction",
"params": { "base": { "select": "kint", "val": "0" } },
"select": { "select": "inside-goal", "occur": 0, "target": "x_0",
"pattern": "$x" },
- "children": { "Base": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ],
- "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ],
- "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ] } } ]
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json
index cf36ff92b88..0abf008d8c2 100644
--- a/src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json
@@ -1,11 +1,10 @@
-[ { "prover": "script", "verdict": "unknown" },
- { "header": "Induction", "tactic": "Wp.induction",
+[ { "header": "Induction", "tactic": "Wp.induction",
"params": { "base": { "select": "kint", "val": "0" } },
"select": { "select": "inside-goal", "occur": 0, "target": "y_0",
"pattern": "$y" },
- "children": { "Base": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ],
- "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ],
- "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ] } } ]
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json b/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json
index e79e12e8f04..a0ac010c2cb 100644
--- a/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json
+++ b/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json
@@ -1,28 +1,27 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.0322 },
- { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
+[ { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "(to_uint32 c_0)", "pattern": "to_uint32$c" },
- "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0082,
- "steps": 32 } ],
- "Lower": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.024,
- "steps": 155 },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.026061,
+ "steps": 22 } ],
+ "Lower": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.031304,
+ "steps": 53 },
{ "header": "Overflow", "tactic": "Wp.overflow",
"params": {},
"select": { "select": "inside-goal",
"occur": 0,
"target": "(to_uint32\n (ui_0+((4294967296+c_0+(-4294967296*(c_0 div 4294967296))) mod 4294967296)))",
"pattern": "to_uint32+$ui%+42949672964294967296" },
- "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.3",
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.0166,
"steps": 27 } ],
- "Lower": [ { "prover": "Alt-Ergo:2.5.3",
+ "Lower": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.023,
"steps": 25 } ],
- "Upper": [ { "prover": "Alt-Ergo:2.5.3",
+ "Upper": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.0739,
"steps": 73 } ] } } ],
diff --git a/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json b/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json
index ae6b0e0b2d2..c76a50b502a 100644
--- a/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json
+++ b/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json
@@ -1,28 +1,27 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.0235 },
- { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
+[ { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "(to_uint32 s_0)", "pattern": "to_uint32$s" },
- "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0069,
- "steps": 32 } ],
- "Lower": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0166,
- "steps": 154 },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.028956,
+ "steps": 22 } ],
+ "Lower": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.030726,
+ "steps": 52 },
{ "header": "Overflow", "tactic": "Wp.overflow",
"params": {},
"select": { "select": "inside-goal",
"occur": 0,
"target": "(to_uint32\n (ui_0+((4294967296+s_0+(-4294967296*(s_0 div 4294967296))) mod 4294967296)))",
"pattern": "to_uint32+$ui%+42949672964294967296" },
- "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.3",
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.017,
"steps": 27 } ],
- "Lower": [ { "prover": "Alt-Ergo:2.5.3",
+ "Lower": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.0232,
"steps": 25 } ],
- "Upper": [ { "prover": "Alt-Ergo:2.5.3",
+ "Upper": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.2614,
"steps": 73 } ] } } ],
--
GitLab