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

[wp] fix some issues with Alt-Ergo

parent 0f324bf5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 77 additions and 413 deletions
nix/default.nix
+ 1
− 1
View file @ c5abda21
...@@ -153,7 +153,7 @@ rec { ...@@ -153,7 +153,7 @@ rec {
wp-qualif = stdenv.mkDerivation { wp-qualif = stdenv.mkDerivation {
name = "frama-c-wp-qualif"; name = "frama-c-wp-qualif";
buildInputs = mk_buildInputs { opamPackages = [ buildInputs = mk_buildInputs { opamPackages = [
{ name = "alt-ergo"; constraint = "=2.2.0"; } { name = "alt-ergo"; constraint = "=2.0.0"; }
]; }; ]; };
build_dir = main.build_dir; build_dir = main.build_dir;
src = main.build_dir + "/dir.tar"; src = main.build_dir + "/dir.tar";
......
src/plugins/wp/tests/wp_gallery/binary-multiplication.c
+ 1
− 1
View file @ c5abda21
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack
*/ */
// The use '-wp-prover=z3,why3:alt-ergo' gives better results. // The use '-wp-prover=z3,why3:alt-ergo' or using Alt-Ergo 2.3.0 gives better results.
typedef unsigned uint32_t ; typedef unsigned uint32_t ;
typedef unsigned long long uint64_t ; typedef unsigned long long uint64_t ;
......
src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+ 4
− 4
View file @ c5abda21
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
[wp] Loading driver 'share/wp.driver' [wp] Loading driver 'share/wp.driver'
[rte] annotating function BinaryMultiplication [rte] annotating function BinaryMultiplication
[wp] 16 goals scheduled [wp] 16 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ax1_lack : Valid [wp] [Alt-Ergo] Goal typed_lemma_ax1_lack : Unsuccess
[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid [wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid [wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid [wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid
...@@ -20,12 +20,12 @@ ...@@ -20,12 +20,12 @@
[wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid [wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid [wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_positive : Valid [wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 16 / 16 [wp] Proved goals: 15 / 16
Qed: 3 Qed: 3
Alt-Ergo: 13 Alt-Ergo: 12 (unsuccess: 1)
------------------------------------------------------------ ------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success Axiomatics WP Alt-Ergo Total Success
Axiomatic mult 1 1 2 100% Axiomatic mult 1 - 2 50.0%
------------------------------------------------------------ ------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
BinaryMultiplication 2 12 14 100% BinaryMultiplication 2 12 14 100%
......
src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+ 4
− 4
View file @ c5abda21
...@@ -10,7 +10,7 @@ ...@@ -10,7 +10,7 @@
[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid [wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid [wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid [wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Valid [wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Unsuccess
[wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid [wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_preserved : Valid [wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_preserved : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_established : Valid [wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_established : Valid
...@@ -21,13 +21,13 @@ ...@@ -21,13 +21,13 @@
[wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid [wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid [wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid [wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 17 / 17 [wp] Proved goals: 16 / 17
Qed: 4 Qed: 4
Alt-Ergo: 13 Alt-Ergo: 12 (unsuccess: 1)
------------------------------------------------------------ ------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success Axiomatics WP Alt-Ergo Total Success
Axiomatic mult 1 3 4 100% Axiomatic mult 1 3 4 100%
------------------------------------------------------------ ------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
BinaryMultiplication 3 10 13 100% BinaryMultiplication 3 9 13 92.3%
------------------------------------------------------------ ------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/nth.i
+ 1
− 2
View file @ c5abda21
/* run.config_qualif /* run.config_qualif
OPT: -wp-prover alt-ergo -wp-prop=-lack OPT:
OPT: -wp-prover why3:alt-ergo
*/ */
/*@ /*@
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+ 1
− 1
View file @ c5abda21
---------------------------------------------------------- ----------------------------------------------------------
WP Requirements for Qualif Tests (3) WP Requirements for Qualif Tests (3)
---------------------------------------------------------- ----------------------------------------------------------
1. The Alt-Ergo theorem prover, version 2.3.0 1. The Alt-Ergo theorem prover, version 2.0.0
2. The Why3 platform, version 1.3.1 2. The Why3 platform, version 1.3.1
3. The Coq Proof Assistant, version 8.11.1 3. The Coq Proof Assistant, version 8.11.1
---------------------------------------------------------- ----------------------------------------------------------
src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+ 1
− 1
View file @ c5abda21
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver' [wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.3.0' [wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.0.0'
[wp] 1 goal scheduled [wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures : Valid [wp] [Alt-Ergo] Goal typed_job_ensures : Valid
[wp] Proved goals: 1 / 1 [wp] Proved goals: 1 / 1
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle deleted 100644 → 0
+ 0
− 15
View file @ 0f324bf5
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/nth.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_access_16_16_ok : Valid
[wp] [Alt-Ergo] Goal typed_lemma_access_4_4_ok : Valid
[wp] [Qed] Goal typed_lemma_eq_repeat_concat_3_ok : Valid
[wp] Proved goals: 3 / 3
Qed: 1
Alt-Ergo: 2
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic Nth 1 2 3 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
+ 4
− 4
View file @ c5abda21
...@@ -6,12 +6,12 @@ ...@@ -6,12 +6,12 @@
[wp] 4 goals scheduled [wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_S : Valid [wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_S : Valid
[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_A : Valid [wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_A : Valid
[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_B : Valid [wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_B : Unsuccess
[wp] [Qed] Goal typed_foo_call_fconcat_requires_qed_ok : Valid [wp] [Qed] Goal typed_foo_call_fconcat_requires_qed_ok : Valid
[wp] Proved goals: 4 / 4 [wp] Proved goals: 3 / 4
Qed: 1 Qed: 1
Alt-Ergo: 3 Alt-Ergo: 2 (unsuccess: 1)
------------------------------------------------------------ ------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
foo 1 3 4 100% foo 1 2 4 75.0%
------------------------------------------------------------ ------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+ 6
− 34
View file @ c5abda21
...@@ -2,37 +2,9 @@ ...@@ -2,37 +2,9 @@
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)", "target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" }, "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.0876, "verdict": "valid", "time": 0.015,
"steps": 51 } ], "steps": 12 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "timeout", "time": 10. }, "verdict": "valid", "time": 0.0156,
{ "header": "Range", "tactic": "Wp.range", "steps": 16 } ] } } ]
"params": { "inf": 0, "sup": 9 },
"select": { "select": "inside-goal",
"occur": 0, "target": "i_102",
"pattern": "$i" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper 9": [ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+ 6
− 34
View file @ c5abda21
...@@ -2,37 +2,9 @@ ...@@ -2,37 +2,9 @@
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)", "target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" }, "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.0876, "verdict": "valid", "time": 0.0148,
"steps": 51 } ], "steps": 12 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "timeout", "time": 10. }, "verdict": "valid", "time": 0.0149,
{ "header": "Range", "tactic": "Wp.range", "steps": 16 } ] } } ]
"params": { "inf": 0, "sup": 9 },
"select": { "select": "inside-goal",
"occur": 0, "target": "i_102",
"pattern": "$i" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper 9": [ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+ 6
− 34
View file @ c5abda21
...@@ -2,37 +2,9 @@ ...@@ -2,37 +2,9 @@
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)", "target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" }, "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.8178, "verdict": "valid", "time": 0.0179,
"steps": 88 } ], "steps": 22 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "timeout", "time": 10. }, "verdict": "valid", "time": 0.0227,
{ "header": "Range", "tactic": "Wp.range", "steps": 28 } ] } } ]
"params": { "inf": 0, "sup": 9 },
"select": { "select": "inside-goal",
"occur": 0, "target": "i_9",
"pattern": "$i" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper 9": [ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+ 6
− 82
View file @ c5abda21
...@@ -2,85 +2,9 @@ ...@@ -2,85 +2,9 @@
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)", "target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" }, "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "timeout", "time": 10. }, "verdict": "valid", "time": 0.0193,
{ "header": "Range", "tactic": "Wp.range", "steps": 16 } ],
"params": { "inf": 0, "sup": 19 }, "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
"select": { "select": "inside-goal", "verdict": "valid", "time": 0.0184,
"occur": 0, "target": "i_3", "steps": 22 } ] } } ]
"pattern": "$i" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 10": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 11": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 12": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 13": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 14": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 15": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 16": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 17": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 18": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 19": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper 19": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 9 },
"select": { "select": "inside-goal",
"occur": 0, "target": "i_0",
"pattern": "$i" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper 9": [ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
+ 6
− 6
View file @ c5abda21
...@@ -2,9 +2,9 @@ ...@@ -2,9 +2,9 @@
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)", "target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" }, "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.0318, "verdict": "valid", "time": 0.0078,
"steps": 39 } ], "steps": 9 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.562, "verdict": "valid", "time": 0.008,
"steps": 414 } ] } } ] "steps": 11 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+ 6
− 34
View file @ c5abda21
...@@ -2,37 +2,9 @@ ...@@ -2,37 +2,9 @@
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)", "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" }, "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.6393, "verdict": "valid", "time": 0.0148,
"steps": 63 } ], "steps": 22 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "timeout", "time": 10. }, "verdict": "valid", "time": 0.0157,
{ "header": "Range", "tactic": "Wp.range", "steps": 24 } ] } } ]
"params": { "inf": 0, "sup": 9 },
"select": { "select": "inside-goal",
"occur": 0, "target": "i_13",
"pattern": "$i" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper 9": [ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+ 6
− 82
View file @ c5abda21
...@@ -2,85 +2,9 @@ ...@@ -2,85 +2,9 @@
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)", "target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" }, "pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "timeout", "time": 10. }, "verdict": "valid", "time": 0.0105,
{ "header": "Range", "tactic": "Wp.range", "steps": 14 } ],
"params": { "inf": 0, "sup": 19 }, "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
"select": { "select": "inside-goal", "verdict": "valid", "time": 0.0144,
"occur": 0, "target": "j_0", "steps": 16 } ] } } ]
"pattern": "$j" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 10": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 11": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 12": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 13": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 14": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 15": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 16": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 17": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 18": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 19": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper 19": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 9 },
"select": { "select": "inside-goal",
"occur": 0, "target": "i_1",
"pattern": "$i" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper 9": [ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+ 6
− 34
View file @ c5abda21
...@@ -2,37 +2,9 @@ ...@@ -2,37 +2,9 @@
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)", "target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" }, "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.4508, "verdict": "valid", "time": 0.0143,
"steps": 55 } ], "steps": 18 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "timeout", "time": 10. }, "verdict": "valid", "time": 0.015,
{ "header": "Range", "tactic": "Wp.range", "steps": 20 } ] } } ]
"params": { "inf": 0, "sup": 9 },
"select": { "select": "inside-goal",
"occur": 0, "target": "i_21",
"pattern": "$i" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper 9": [ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+ 6
− 34
View file @ c5abda21
...@@ -2,37 +2,9 @@ ...@@ -2,37 +2,9 @@
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)", "target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" }, "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.4508, "verdict": "valid", "time": 0.0148,
"steps": 55 } ], "steps": 18 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "timeout", "time": 10. }, "verdict": "valid", "time": 0.0153,
{ "header": "Range", "tactic": "Wp.range", "steps": 20 } ] } } ]
"params": { "inf": 0, "sup": 9 },
"select": { "select": "inside-goal",
"occur": 0, "target": "i_8",
"pattern": "$i" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper 9": [ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
+ 6
− 6
View file @ c5abda21
...@@ -2,9 +2,9 @@ ...@@ -2,9 +2,9 @@
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)", "target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" }, "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.0318, "verdict": "valid", "time": 0.0079,
"steps": 39 } ], "steps": 9 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.562, "verdict": "valid", "time": 0.0082,
"steps": 414 } ] } } ] "steps": 11 } ] } } ]
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