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

[wp/qualif] update prover titles

parent 6a2d170d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 29 additions and 29 deletions
src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
+ 2
− 2
View file @ 1ac023d0
...@@ -7,8 +7,8 @@ ...@@ -7,8 +7,8 @@
[wp] [alt-ergo] Goal typed_lemma_InfP_not_finite : Valid [wp] [alt-ergo] Goal typed_lemma_InfP_not_finite : Valid
[wp] [alt-ergo] Goal typed_lemma_NaN_not_finite : Valid [wp] [alt-ergo] Goal typed_lemma_NaN_not_finite : Valid
[wp] Proved goals: 3 / 3 [wp] Proved goals: 3 / 3
Qed: 0 Qed: 0
alt-ergo: 3 Alt-Ergo (why3): 3
[wp] Report in: 'tests/wp_acsl/oracle_qualif/classify_float.1.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/classify_float.1.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/classify_float.1.report.json' [wp] Report out: 'tests/wp_acsl/result_qualif/classify_float.1.report.json'
------------------------------------------------------------- -------------------------------------------------------------
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
+ 2
− 2
View file @ 1ac023d0
...@@ -27,8 +27,8 @@ ...@@ -27,8 +27,8 @@
[wp] [alt-ergo] Goal typed_f_ensures_sm2_mod_pos_neg : Valid [wp] [alt-ergo] Goal typed_f_ensures_sm2_mod_pos_neg : Valid
[wp] [alt-ergo] Goal typed_f_ensures_sm3_mod_neg_neg : Valid [wp] [alt-ergo] Goal typed_f_ensures_sm3_mod_neg_neg : Valid
[wp] Proved goals: 22 / 22 [wp] Proved goals: 22 / 22
Qed: 0 Qed: 0
alt-ergo: 22 Alt-Ergo (why3): 22
[wp] Report in: 'tests/wp_acsl/oracle_qualif/div_mod.1.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/div_mod.1.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/div_mod.1.report.json' [wp] Report out: 'tests/wp_acsl/result_qualif/div_mod.1.report.json'
------------------------------------------------------------- -------------------------------------------------------------
......
src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
+ 5
− 5
View file @ 1ac023d0
...@@ -5,17 +5,17 @@ ...@@ -5,17 +5,17 @@
[wp] 2 goals scheduled [wp] 2 goals scheduled
[wp] [Coq] Goal typed_lemma_ok_because_inconsistent : Default tactic [wp] [Coq] Goal typed_lemma_ok_because_inconsistent : Default tactic
[wp] [Failed] Goal typed_lemma_ok_because_inconsistent [wp] [Failed] Goal typed_lemma_ok_because_inconsistent
alt-ergo: Failed Command './tests/inexistant-prover' not found Alt-Ergo (why3): Failed Command './tests/inexistant-prover' not found
Coq: Failed Command './tests/inexistant-prover' not found Coq: Failed Command './tests/inexistant-prover' not found
Alt-Ergo: Failed Command './tests/inexistant-prover' not found Alt-Ergo: Failed Command './tests/inexistant-prover' not found
[wp] [Failed] Goal typed_lemma_ok_because_consistent [wp] [Failed] Goal typed_lemma_ok_because_consistent
alt-ergo: Failed Command './tests/inexistant-prover' not found Alt-Ergo (why3): Failed Command './tests/inexistant-prover' not found
Coq: Failed Command './tests/inexistant-prover' not found Coq: Failed Command './tests/inexistant-prover' not found
Alt-Ergo: Failed Command './tests/inexistant-prover' not found Alt-Ergo: Failed Command './tests/inexistant-prover' not found
[wp] Proved goals: 0 / 2 [wp] Proved goals: 0 / 2
Alt-Ergo: 0 (failed: 2) Alt-Ergo: 0 (failed: 2)
Coq: 0 (failed: 2) Coq: 0 (failed: 2)
alt-ergo: 0 (failed: 2) Alt-Ergo (why3): 0 (failed: 2)
[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_143.1.report.json' [wp] Report in: 'tests/wp_bts/oracle_qualif/issue_143.1.report.json'
[wp] Report out: 'tests/wp_bts/result_qualif/issue_143.1.report.json' [wp] Report out: 'tests/wp_bts/result_qualif/issue_143.1.report.json'
------------------------------------------------------------- -------------------------------------------------------------
......
src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+ 4
− 4
View file @ 1ac023d0
...@@ -15,8 +15,8 @@ ...@@ -15,8 +15,8 @@
[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: 10 / 10 [wp] Proved goals: 10 / 10
Qed: 3 Qed: 3
alt-ergo: 7 Alt-Ergo (why3): 7
[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.report.json' [wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.report.json'
[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication-without-overflow.0.report.json' [wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication-without-overflow.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
...@@ -44,8 +44,8 @@ BinaryMultiplication 2 - 9 100% ...@@ -44,8 +44,8 @@ BinaryMultiplication 2 - 9 100%
[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: 11 / 14 [wp] Proved goals: 11 / 14
Qed: 0 Qed: 0
alt-ergo: 11 Alt-Ergo (why3): 11
[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.report.json' [wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.report.json'
[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication-without-overflow.0.report.json' [wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication-without-overflow.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
......
src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+ 4
− 4
View file @ 1ac023d0
...@@ -22,8 +22,8 @@ ...@@ -22,8 +22,8 @@
[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: 17 / 17
Qed: 4 Qed: 4
alt-ergo: 13 Alt-Ergo (why3): 13
[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication.0.report.json' [wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication.0.report.json'
[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication.0.report.json' [wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
...@@ -54,8 +54,8 @@ BinaryMultiplication 3 - 13 100% ...@@ -54,8 +54,8 @@ BinaryMultiplication 3 - 13 100%
[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: 13 / 17 [wp] Proved goals: 13 / 17
Qed: 0 Qed: 0
alt-ergo: 13 Alt-Ergo (why3): 13
[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication.0.report.json' [wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication.0.report.json'
[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication.0.report.json' [wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
+ 2
− 2
View file @ 1ac023d0
...@@ -6,8 +6,8 @@ ...@@ -6,8 +6,8 @@
[wp] 1 goal scheduled [wp] 1 goal scheduled
[wp] [alt-ergo] Goal typed_abs_abs_ensures : Valid [wp] [alt-ergo] Goal typed_abs_abs_ensures : Valid
[wp] Proved goals: 1 / 1 [wp] Proved goals: 1 / 1
Qed: 0 Qed: 0
alt-ergo: 1 Alt-Ergo (why3): 1
[wp] Report in: 'tests/wp_plugin/oracle_qualif/abs.2.report.json' [wp] Report in: 'tests/wp_plugin/oracle_qualif/abs.2.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/abs.2.report.json' [wp] Report out: 'tests/wp_plugin/result_qualif/abs.2.report.json'
------------------------------------------------------------- -------------------------------------------------------------
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
+ 2
− 2
View file @ 1ac023d0
...@@ -6,8 +6,8 @@ ...@@ -6,8 +6,8 @@
[wp] [alt-ergo] Goal typed_lemma_ceil : Valid [wp] [alt-ergo] Goal typed_lemma_ceil : Valid
[wp] [alt-ergo] Goal typed_lemma_floor : Valid [wp] [alt-ergo] Goal typed_lemma_floor : Valid
[wp] Proved goals: 2 / 2 [wp] Proved goals: 2 / 2
Qed: 0 Qed: 0
alt-ergo: 2 Alt-Ergo (why3): 2
---------------------------------------------------------- ----------------------------------------------------------
Axiomatics WP Alt-Ergo(Why3) Total Success Axiomatics WP Alt-Ergo(Why3) Total Success
Lemma - 2 2 100% Lemma - 2 2 100%
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
+ 1
− 1
View file @ 1ac023d0
...@@ -9,7 +9,7 @@ ...@@ -9,7 +9,7 @@
[wp] 1 goal scheduled [wp] 1 goal scheduled
[wp] [alt-ergo] Goal typed_output_ensures_KO : Unsuccess [wp] [alt-ergo] Goal typed_output_ensures_KO : Unsuccess
[wp] Proved goals: 0 / 1 [wp] Proved goals: 0 / 1
alt-ergo: 0 (unsuccess: 1) Alt-Ergo (why3): 0 (unsuccess: 1)
[wp] Report in: 'tests/wp_plugin/oracle_qualif/float_format.2.report.json' [wp] Report in: 'tests/wp_plugin/oracle_qualif/float_format.2.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/float_format.2.report.json' [wp] Report out: 'tests/wp_plugin/result_qualif/float_format.2.report.json'
------------------------------------------------------------- -------------------------------------------------------------
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
+ 2
− 2
View file @ 1ac023d0
...@@ -35,8 +35,8 @@ ...@@ -35,8 +35,8 @@
[wp] [alt-ergo] Goal typed_ok_ensures_sqrt_pos : Valid [wp] [alt-ergo] Goal typed_ok_ensures_sqrt_pos : Valid
[wp] [alt-ergo] Goal typed_ok_ensures_sqrt_pos0 : Valid [wp] [alt-ergo] Goal typed_ok_ensures_sqrt_pos0 : Valid
[wp] Proved goals: 30 / 30 [wp] Proved goals: 30 / 30
Qed: 5 Qed: 5
alt-ergo: 25 Alt-Ergo (why3): 25
---------------------------------------------------------- ----------------------------------------------------------
Axiomatics WP Alt-Ergo(Why3) Total Success Axiomatics WP Alt-Ergo(Why3) Total Success
Lemma 3 16 19 100% Lemma 3 16 19 100%
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
+ 1
− 1
View file @ 1ac023d0
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
[wp] [alt-ergo] Goal typed_ko_ensures_ko_exp_log_add_mul : Unsuccess [wp] [alt-ergo] Goal typed_ko_ensures_ko_exp_log_add_mul : Unsuccess
[wp] [alt-ergo] Goal typed_ko_ensures_ko_sqrt_pos : Unsuccess [wp] [alt-ergo] Goal typed_ko_ensures_ko_sqrt_pos : Unsuccess
[wp] Proved goals: 0 / 9 [wp] Proved goals: 0 / 9
alt-ergo: 0 (unsuccess: 9) Alt-Ergo (why3): 0 (unsuccess: 9)
---------------------------------------------------------- ----------------------------------------------------------
Functions WP Alt-Ergo(Why3) Total Success Functions WP Alt-Ergo(Why3) Total Success
ko - - 9 0.0% ko - - 9 0.0%
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
+ 2
− 2
View file @ 1ac023d0
...@@ -8,8 +8,8 @@ ...@@ -8,8 +8,8 @@
[wp] [alt-ergo] Goal typed_lemma_access_repeat_concat_3_ok_lack : Valid [wp] [alt-ergo] Goal typed_lemma_access_repeat_concat_3_ok_lack : Valid
[wp] [Qed] Goal typed_lemma_eq_repeat_concat_3_ok : Valid [wp] [Qed] Goal typed_lemma_eq_repeat_concat_3_ok : Valid
[wp] Proved goals: 4 / 4 [wp] Proved goals: 4 / 4
Qed: 1 Qed: 1
alt-ergo: 3 Alt-Ergo (why3): 3
[wp] Report in: 'tests/wp_plugin/oracle_qualif/nth.1.report.json' [wp] Report in: 'tests/wp_plugin/oracle_qualif/nth.1.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/nth.1.report.json' [wp] Report out: 'tests/wp_plugin/result_qualif/nth.1.report.json'
------------------------------------------------------------- -------------------------------------------------------------
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
+ 2
− 2
View file @ 1ac023d0
...@@ -39,8 +39,8 @@ ...@@ -39,8 +39,8 @@
[wp] [Qed] Goal typed_caveat_sequence_g_not_called_ensures_ok_q2 : Valid [wp] [Qed] Goal typed_caveat_sequence_g_not_called_ensures_ok_q2 : Valid
[wp] [alt-ergo] Goal typed_caveat_sequence_g_not_called_ensures_ok_q3 : Valid [wp] [alt-ergo] Goal typed_caveat_sequence_g_not_called_ensures_ok_q3 : Valid
[wp] Proved goals: 34 / 34 [wp] Proved goals: 34 / 34
Qed: 22 Qed: 22
alt-ergo: 12 Alt-Ergo (why3): 12
[wp] Report in: 'tests/wp_plugin/oracle_qualif/sequence.1.report.json' [wp] Report in: 'tests/wp_plugin/oracle_qualif/sequence.1.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/sequence.1.report.json' [wp] Report out: 'tests/wp_plugin/result_qualif/sequence.1.report.json'
------------------------------------------------------------- -------------------------------------------------------------
......
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