From 1ac023d0c349534e16249b202caef07bd22b0473 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 24 Apr 2019 15:01:57 +0200
Subject: [PATCH] [wp/qualif] update prover titles
---
.../wp_acsl/oracle_qualif/classify_float.1.res.oracle | 4 ++--
.../tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle | 4 ++--
.../tests/wp_bts/oracle_qualif/issue_143.1.res.oracle | 10 +++++-----
.../binary-multiplication-without-overflow.res.oracle | 8 ++++----
.../oracle_qualif/binary-multiplication.res.oracle | 8 ++++----
.../wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle | 4 ++--
.../tests/wp_plugin/oracle_qualif/convert.1.res.oracle | 4 ++--
.../wp_plugin/oracle_qualif/float_format.2.res.oracle | 2 +-
.../wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle | 4 ++--
.../wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle | 2 +-
.../wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle | 4 ++--
.../wp_plugin/oracle_qualif/sequence.1.res.oracle | 4 ++--
12 files changed, 29 insertions(+), 29 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
index 7c556d41418..0b99ce986f7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
@@ -7,8 +7,8 @@
[wp] [alt-ergo] Goal typed_lemma_InfP_not_finite : Valid
[wp] [alt-ergo] Goal typed_lemma_NaN_not_finite : Valid
[wp] Proved goals: 3 / 3
- Qed: 0
- alt-ergo: 3
+ Qed: 0
+ Alt-Ergo (why3): 3
[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'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
index 282eb4ee097..b6f8e5f4ca8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
@@ -27,8 +27,8 @@
[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] Proved goals: 22 / 22
- Qed: 0
- alt-ergo: 22
+ Qed: 0
+ Alt-Ergo (why3): 22
[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'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
index 2da222911d1..bb43d9e7d04 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
@@ -5,17 +5,17 @@
[wp] 2 goals scheduled
[wp] [Coq] Goal typed_lemma_ok_because_inconsistent : Default tactic
[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
Alt-Ergo: Failed Command './tests/inexistant-prover' not found
[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
Alt-Ergo: Failed Command './tests/inexistant-prover' not found
[wp] Proved goals: 0 / 2
- Alt-Ergo: 0 (failed: 2)
- Coq: 0 (failed: 2)
- alt-ergo: 0 (failed: 2)
+ Alt-Ergo: 0 (failed: 2)
+ Coq: 0 (failed: 2)
+ Alt-Ergo (why3): 0 (failed: 2)
[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'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
index 396326b005b..cfdf8aa1564 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
@@ -15,8 +15,8 @@
[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 10 / 10
- Qed: 3
- alt-ergo: 7
+ Qed: 3
+ Alt-Ergo (why3): 7
[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'
-------------------------------------------------------------
@@ -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_positive : Valid
[wp] Proved goals: 11 / 14
- Qed: 0
- alt-ergo: 11
+ Qed: 0
+ Alt-Ergo (why3): 11
[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'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index df6617e5ab9..65f0dab3fc4 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -22,8 +22,8 @@
[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 17 / 17
- Qed: 4
- alt-ergo: 13
+ Qed: 4
+ Alt-Ergo (why3): 13
[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'
-------------------------------------------------------------
@@ -54,8 +54,8 @@ BinaryMultiplication 3 - 13 100%
[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 13 / 17
- Qed: 0
- alt-ergo: 13
+ Qed: 0
+ Alt-Ergo (why3): 13
[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'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
index a1093f1b486..4e80668bd54 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
@@ -6,8 +6,8 @@
[wp] 1 goal scheduled
[wp] [alt-ergo] Goal typed_abs_abs_ensures : Valid
[wp] Proved goals: 1 / 1
- Qed: 0
- alt-ergo: 1
+ Qed: 0
+ Alt-Ergo (why3): 1
[wp] Report in: 'tests/wp_plugin/oracle_qualif/abs.2.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/abs.2.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
index 6a81ceb4c39..90b1a19b299 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
@@ -6,8 +6,8 @@
[wp] [alt-ergo] Goal typed_lemma_ceil : Valid
[wp] [alt-ergo] Goal typed_lemma_floor : Valid
[wp] Proved goals: 2 / 2
- Qed: 0
- alt-ergo: 2
+ Qed: 0
+ Alt-Ergo (why3): 2
----------------------------------------------------------
Axiomatics WP Alt-Ergo(Why3) Total Success
Lemma - 2 2 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
index f2836be71fc..fbad8e13cb9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
@@ -9,7 +9,7 @@
[wp] 1 goal scheduled
[wp] [alt-ergo] Goal typed_output_ensures_KO : Unsuccess
[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 out: 'tests/wp_plugin/result_qualif/float_format.2.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
index bf2477d381d..239622cf211 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
@@ -35,8 +35,8 @@
[wp] [alt-ergo] Goal typed_ok_ensures_sqrt_pos : Valid
[wp] [alt-ergo] Goal typed_ok_ensures_sqrt_pos0 : Valid
[wp] Proved goals: 30 / 30
- Qed: 5
- alt-ergo: 25
+ Qed: 5
+ Alt-Ergo (why3): 25
----------------------------------------------------------
Axiomatics WP Alt-Ergo(Why3) Total Success
Lemma 3 16 19 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
index c8da0ce7146..b36de4de9c7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
@@ -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_sqrt_pos : Unsuccess
[wp] Proved goals: 0 / 9
- alt-ergo: 0 (unsuccess: 9)
+ Alt-Ergo (why3): 0 (unsuccess: 9)
----------------------------------------------------------
Functions WP Alt-Ergo(Why3) Total Success
ko - - 9 0.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
index 6f80bff20c4..96da4b6f6ab 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
@@ -8,8 +8,8 @@
[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] Proved goals: 4 / 4
- Qed: 1
- alt-ergo: 3
+ Qed: 1
+ Alt-Ergo (why3): 3
[wp] Report in: 'tests/wp_plugin/oracle_qualif/nth.1.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/nth.1.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
index e2333a2acdc..922a6a40b60 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
@@ -39,8 +39,8 @@
[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] Proved goals: 34 / 34
- Qed: 22
- alt-ergo: 12
+ Qed: 22
+ Alt-Ergo (why3): 12
[wp] Report in: 'tests/wp_plugin/oracle_qualif/sequence.1.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/sequence.1.report.json'
-------------------------------------------------------------
--
GitLab