Skip to content
Snippets Groups Projects
Commit b003e55f authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] updated oracles & scripts

parent d391280b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 82 additions and 70 deletions
src/plugins/wp/tests/why3/test_config_qualif
+ 1
− 1
View file @ b003e55f
FILEREG: .*\.why FILEREG: .*\.why
DEPS: ~/.why3.conf 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: OPT:
COMMENT: the filter remove the information about time and steps COMMENT: the filter remove the information about time and steps
FILTER: sed -e 's|\(.*\)\( (.*)\)|\1|' FILTER: sed -e 's|\(.*\)\( (.*)\)|\1|'
src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json
+ 4
− 5
View file @ b003e55f
[ { "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, "select": { "select": "inside-step", "at": 1, "kind": "have", "occur": 0,
"target": "not (bit_test off_0 15)", "target": "not (bit_test off_0 15)",
"pattern": "!bit_test$off15" }, "pattern": "!bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "qed", "verdict": "valid" } ], "children": { "Bit #15 (inf)": [ { "prover": "qed", "verdict": "valid" } ],
"Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.5.3", "Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "time": 0.0204, "verdict": "valid", "time": 0.027549,
"steps": 52 } ] } } ] "steps": 38 } ] } } ]
src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json
+ 4
− 5
View file @ b003e55f
[ { "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, "select": { "select": "inside-step", "at": 1, "kind": "have", "occur": 0,
"target": "(bit_test off_0 15)", "target": "(bit_test off_0 15)",
"pattern": "bit_test$off15" }, "pattern": "bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.5.3", "children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "time": 0.0194, "verdict": "valid", "time": 0.021835,
"steps": 52 } ], "steps": 37 } ],
"Bit #15 (sup)": [ { "prover": "qed", "verdict": "valid" } ] } } ] "Bit #15 (sup)": [ { "prover": "qed", "verdict": "valid" } ] } } ]
src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+ 2
− 2
View file @ b003e55f
---------------------------------------------------------- ----------------------------------------------------------
WP Requirements for Qualif Tests WP Requirements for Qualif Tests
---------------------------------------------------------- ----------------------------------------------------------
1. The Alt-Ergo theorem prover, version v2.5.3 1. The Alt-Ergo theorem prover, version v2.5.4
2. The Why3 platform, version 1.7.1 2. The Why3 platform, version 1.7.2
3. The environment variable FRAMAC_WP_CACHEDIR is defined 3. The environment variable FRAMAC_WP_CACHEDIR is defined
4. The environment variable FRAMAC_WP_CACHE is defined 4. The environment variable FRAMAC_WP_CACHE is defined
---------------------------------------------------------- ----------------------------------------------------------
src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+ 1
− 1
View file @ b003e55f
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
[wp] [Valid] Goal job_terminates (Cfg) (Trivial) [wp] [Valid] Goal job_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] 1 goal scheduled [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] [Valid] typed_job_ensures (Alt-Ergo) (Cached)
[wp] Proved goals: 3 / 3 [wp] Proved goals: 3 / 3
Terminating: 1 Terminating: 1
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+ 4
− 4
View file @ b003e55f
...@@ -2,10 +2,10 @@ ...@@ -2,10 +2,10 @@
[kernel] Parsing unsigned.i (no preprocessing) [kernel] Parsing unsigned.i (no preprocessing)
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] 1 goal scheduled [wp] 1 goal scheduled
[wp] [Unsuccess] typed_lemma_U32 (Tactic) (Qed 1/2) [wp] [Valid] typed_lemma_U32 (Tactics 3) (Qed 4/4)
[wp] Proved goals: 0 / 1 [wp] Proved goals: 1 / 1
Unsuccess: 1 Script: 1 (Tactics 3) (Qed 4/4)
------------------------------------------------------------ ------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success Axiomatics WP Alt-Ergo Total Success
Lemma - - 1 0.0% Lemma - - 1 100%
------------------------------------------------------------ ------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json
+ 23
− 4
View file @ b003e55f
[ { "prover": "script", "verdict": "unknown" }, [ { "header": "Bitwise Eq.", "tactic": "Wp.bitwised",
{ "header": "Bitwise Eq.", "tactic": "Wp.bitwised",
"params": { "Wp.bitwised.range": 32 }, "params": { "Wp.bitwised.range": 32 },
"select": { "select": "clause-goal", "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": [ { "prover": "Alt-Ergo:2.5.3", "children": { "range": [ { "header": "Split", "tactic": "Wp.split",
"verdict": "timeout", "time": 10. } ], "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" } ] } } ] "bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json
+ 9
− 10
View file @ b003e55f
[ { "prover": "script", "verdict": "valid", "time": 0.04 }, [ { "header": "Induction", "tactic": "Wp.induction",
{ "header": "Induction", "tactic": "Wp.induction",
"params": { "base": { "select": "kint", "val": "0" } }, "params": { "base": { "select": "kint", "val": "0" } },
"select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)", "select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
"pattern": "L_f$x" }, "pattern": "L_f$x" },
"children": { "Base": [ { "prover": "Alt-Ergo:2.5.3", "verdict": "valid", "children": { "Base": [ { "prover": "Alt-Ergo:2.5.4", "verdict": "valid",
"time": 0.0035, "steps": 14 } ], "time": 0.013909, "steps": 4 } ],
"Induction (sup)": [ { "prover": "Alt-Ergo:2.5.3", "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "time": 0.0247, "verdict": "valid", "time": 0.02138,
"steps": 325 } ], "steps": 88 } ],
"Induction (inf)": [ { "prover": "Alt-Ergo:2.5.3", "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "time": 0.0118, "verdict": "valid",
"steps": 32 } ] } } ] "time": 0.026118, "steps": 116 } ] } } ]
src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json
+ 7
− 8
View file @ b003e55f
[ { "prover": "script", "verdict": "unknown" }, [ { "header": "Induction", "tactic": "Wp.induction",
{ "header": "Induction", "tactic": "Wp.induction",
"params": { "base": { "select": "kint", "val": "0" } }, "params": { "base": { "select": "kint", "val": "0" } },
"select": { "select": "inside-goal", "occur": 0, "target": "x_0", "select": { "select": "inside-goal", "occur": 0, "target": "x_0",
"pattern": "$x" }, "pattern": "$x" },
"children": { "Base": [ { "prover": "Alt-Ergo:2.5.3", "children": { "Base": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "timeout", "time": 10. } ], "verdict": "timeout", "time": 1. } ],
"Induction (sup)": [ { "prover": "Alt-Ergo:2.5.3", "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "timeout", "time": 10. } ], "verdict": "timeout", "time": 1. } ],
"Induction (inf)": [ { "prover": "Alt-Ergo:2.5.3", "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "timeout", "time": 10. } ] } } ] "verdict": "timeout", "time": 1. } ] } } ]
src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json
+ 7
− 8
View file @ b003e55f
[ { "prover": "script", "verdict": "unknown" }, [ { "header": "Induction", "tactic": "Wp.induction",
{ "header": "Induction", "tactic": "Wp.induction",
"params": { "base": { "select": "kint", "val": "0" } }, "params": { "base": { "select": "kint", "val": "0" } },
"select": { "select": "inside-goal", "occur": 0, "target": "y_0", "select": { "select": "inside-goal", "occur": 0, "target": "y_0",
"pattern": "$y" }, "pattern": "$y" },
"children": { "Base": [ { "prover": "Alt-Ergo:2.5.3", "children": { "Base": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "timeout", "time": 10. } ], "verdict": "timeout", "time": 1. } ],
"Induction (sup)": [ { "prover": "Alt-Ergo:2.5.3", "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "timeout", "time": 10. } ], "verdict": "timeout", "time": 1. } ],
"Induction (inf)": [ { "prover": "Alt-Ergo:2.5.3", "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "timeout", "time": 10. } ] } } ] "verdict": "timeout", "time": 1. } ] } } ]
src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json
+ 10
− 11
View file @ b003e55f
[ { "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, "select": { "select": "inside-goal", "occur": 0,
"target": "(to_uint32 c_0)", "pattern": "to_uint32$c" }, "target": "(to_uint32 c_0)", "pattern": "to_uint32$c" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.3", "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "time": 0.0082, "verdict": "valid", "time": 0.026061,
"steps": 32 } ], "steps": 22 } ],
"Lower": [ { "prover": "Alt-Ergo:2.5.3", "Lower": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "time": 0.024, "verdict": "valid", "time": 0.031304,
"steps": 155 }, "steps": 53 },
{ "header": "Overflow", "tactic": "Wp.overflow", { "header": "Overflow", "tactic": "Wp.overflow",
"params": {}, "params": {},
"select": { "select": "inside-goal", "select": { "select": "inside-goal",
"occur": 0, "occur": 0,
"target": "(to_uint32\n (ui_0+((4294967296+c_0+(-4294967296*(c_0 div 4294967296))) mod 4294967296)))", "target": "(to_uint32\n (ui_0+((4294967296+c_0+(-4294967296*(c_0 div 4294967296))) mod 4294967296)))",
"pattern": "to_uint32+$ui%+42949672964294967296" }, "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", "verdict": "valid",
"time": 0.0166, "time": 0.0166,
"steps": 27 } ], "steps": 27 } ],
"Lower": [ { "prover": "Alt-Ergo:2.5.3", "Lower": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "verdict": "valid",
"time": 0.023, "time": 0.023,
"steps": 25 } ], "steps": 25 } ],
"Upper": [ { "prover": "Alt-Ergo:2.5.3", "Upper": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "verdict": "valid",
"time": 0.0739, "time": 0.0739,
"steps": 73 } ] } } ], "steps": 73 } ] } } ],
......
src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json
+ 10
− 11
View file @ b003e55f
[ { "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, "select": { "select": "inside-goal", "occur": 0,
"target": "(to_uint32 s_0)", "pattern": "to_uint32$s" }, "target": "(to_uint32 s_0)", "pattern": "to_uint32$s" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.3", "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "time": 0.0069, "verdict": "valid", "time": 0.028956,
"steps": 32 } ], "steps": 22 } ],
"Lower": [ { "prover": "Alt-Ergo:2.5.3", "Lower": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "time": 0.0166, "verdict": "valid", "time": 0.030726,
"steps": 154 }, "steps": 52 },
{ "header": "Overflow", "tactic": "Wp.overflow", { "header": "Overflow", "tactic": "Wp.overflow",
"params": {}, "params": {},
"select": { "select": "inside-goal", "select": { "select": "inside-goal",
"occur": 0, "occur": 0,
"target": "(to_uint32\n (ui_0+((4294967296+s_0+(-4294967296*(s_0 div 4294967296))) mod 4294967296)))", "target": "(to_uint32\n (ui_0+((4294967296+s_0+(-4294967296*(s_0 div 4294967296))) mod 4294967296)))",
"pattern": "to_uint32+$ui%+42949672964294967296" }, "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", "verdict": "valid",
"time": 0.017, "time": 0.017,
"steps": 27 } ], "steps": 27 } ],
"Lower": [ { "prover": "Alt-Ergo:2.5.3", "Lower": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "verdict": "valid",
"time": 0.0232, "time": 0.0232,
"steps": 25 } ], "steps": 25 } ],
"Upper": [ { "prover": "Alt-Ergo:2.5.3", "Upper": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid", "verdict": "valid",
"time": 0.2614, "time": 0.2614,
"steps": 73 } ] } } ], "steps": 73 } ] } } ],
......
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