From cfdeee3a741b0188173315e4fec660db4c0694a6 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 10 Jan 2022 17:41:16 +0100
Subject: [PATCH] [wp] Update tests oracles
---
.../wp_bts/oracle_qualif/issue_751.res.oracle | 4 +--
.../unsigned.0.session/script/lemma_U32.json | 35 ++++---------------
2 files changed, 9 insertions(+), 30 deletions(-)
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
index c3ac6213cb4..69f63c6e1c9 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
@@ -3,10 +3,10 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 40 goals scheduled
-[wp] [Alt-Ergo] Goal typed_acquire_loop_invariant_RANGE_preserved : Valid (Qed:3ms) (17ms) (39) (missing cache)
+[wp] [Alt-Ergo] Goal typed_acquire_loop_invariant_RANGE_preserved : Valid
[wp] [Qed] Goal typed_acquire_loop_invariant_RANGE_established : Valid
[wp] [Qed] Goal typed_acquire_loop_assigns_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_acquire_loop_assigns_part2 : Valid (Qed:5ms) (18ms) (52) (missing cache)
+[wp] [Alt-Ergo] Goal typed_acquire_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_issue_751_check : Valid
[wp] [Qed] Goal typed_issue_751_check_2 : Valid
[wp] [Qed] Goal typed_issue_751_check_3 : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
index 77438629a17..c4a3730943a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
@@ -1,32 +1,11 @@
-[ { "header": "Bitwise Eq.", "tactic": "Wp.bitwised",
+[ { "prover": "Alt-Ergo:2.2.0", "verdict": "timeout", "time": 10. },
+ { "prover": "script", "verdict": "valid" },
+ { "header": "Bitwise Eq.", "tactic": "Wp.bitwised",
"params": { "Wp.bitwised.range": 32 },
- "select": { "select": "inside-goal", "occur": 0,
+ "select": { "select": "clause-goal",
"target": "(land 4294967295 x_0)=x_0",
"pattern": "=land$x4294967295$x" },
- "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": "Alt-Ergo:2.2.0",
- "verdict": "valid",
- "time": 0.0095,
- "steps": 14 } ],
- "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": "Alt-Ergo:2.2.0",
- "verdict": "valid",
- "time": 0.01,
- "steps": 14 } ] } } ],
+ "children": { "range": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0054,
+ "steps": 15 } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
--
GitLab