Skip to content
Snippets Groups Projects
Commit cfdeee3a authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Update tests oracles

parent 7f032791
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
+ 2
− 2
View file @ cfdeee3a
...@@ -3,10 +3,10 @@ ...@@ -3,10 +3,10 @@
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] 40 goals scheduled [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_invariant_RANGE_established : Valid
[wp] [Qed] Goal typed_acquire_loop_assigns_part1 : 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 : Valid
[wp] [Qed] Goal typed_issue_751_check_2 : Valid [wp] [Qed] Goal typed_issue_751_check_2 : Valid
[wp] [Qed] Goal typed_issue_751_check_3 : Valid [wp] [Qed] Goal typed_issue_751_check_3 : Valid
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
+ 7
− 28
View file @ cfdeee3a
[ { "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 }, "params": { "Wp.bitwised.range": 32 },
"select": { "select": "inside-goal", "occur": 0, "select": { "select": "clause-goal",
"target": "(land 4294967295 x_0)=x_0", "target": "(land 4294967295 x_0)=x_0",
"pattern": "=land$x4294967295$x" }, "pattern": "=land$x4294967295$x" },
"children": { "range": [ { "header": "Split", "tactic": "Wp.split", "children": { "range": [ { "prover": "Alt-Ergo:2.2.0",
"params": {}, "verdict": "valid", "time": 0.0054,
"select": { "select": "clause-goal", "steps": 15 } ],
"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 } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ] "bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment