diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c b/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c
index 3b2f455462b87e1a1583e00411d232de30245661..c1946eee14500d6db0d7df208a37e2855406e974 100644
--- a/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c
+++ b/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c
@@ -3,30 +3,29 @@
*/
/* run.config_qualif
- OPT: -warn-unsigned-overflow -wp-prop=-lack -then -warn-unsigned-overflow -wp-rte -wp -wp-prop=-lack
+ OPT: -wp-prover why3:alt-ergo -warn-unsigned-overflow -wp-prop=-lack -then -warn-unsigned-overflow -wp-rte -wp -wp-prop=-lack
*/
typedef unsigned uint32_t ;
typedef unsigned long long uint64_t ;
/*@ axiomatic mult {
- @ lemma sizeof_uint32_t: ok: sizeof(uint32_t) == 4; // 4 bytes: 32 bits
- @ lemma sizeof_uint64_t: ok: sizeof(uint64_t) == 8; // 8 bytes: 64 bits
- @
- @ lemma ax1: lack: \forall integer x, y; 0<=x && 0< y ==> 0 <= x <= x*y;
- @ lemma ax2: lack: \forall integer x, y; 0<=x && 0<=y ==> 0 <= 2*x*(y/2) <= x*y;
+
+ @ lemma sizeof_ok: ok: sizeof(uint64_t) == 2 * sizeof(uint32_t);
+
+ @ lemma ax1: lack: \forall integer x, y; 0<x && 0<y ==> 0 <= 2*x*(y/2) <= x*y;
@ }
@ */
//@ ensures product: \result == a*b;
uint64_t BinaryMultiplication (uint32_t a, uint32_t b) {
- //@ assert a1: ok: deductible: a*b <= 18446744073709551615; // deductible from type size
+ //@ assert a1: ok: deductible: a*b <= 18446744073709551615; // deductible from size of C types
uint64_t r=0;
uint64_t x=a;
if (b != 0) {
/*@ loop assigns ok: r, x, b;
- @ loop invariant inv1: lack: r+x*b == \at(a*b, LoopEntry);
- @ loop invariant inv2: ok: deductible: 2*x*(b/2) <= 18446744073709551615; // deductible from inv1, ax2, ax1, a1 and x>=0, b>0, r>=0
+ @ loop invariant inv1: ok: r+x*b == \at(a*b, LoopEntry);
+ @ loop invariant inv2: ok: deductible: 2*x*(b/2) <= 18446744073709551615; // deductible from inv1, ax1, a1 and x>=0, b>0, r>=0
@ loop variant ok: b ;
@*/
while (1) {
diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json b/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json
index e5cea006b893c57b97b6bce5b539a95158f1c2a9..fd14edb93a62ed85f22868b68e6d12c0ab84415b 100644
--- a/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json
+++ b/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json
@@ -1,89 +1,72 @@
-{ "wp:global": { "alt-ergo": { "total": 10, "valid": 10, "rank": 17 },
+{ "wp:global": { "why3:alt-ergo": { "total": 11, "valid": 11 },
"qed": { "total": 3, "valid": 3 },
- "wp:main": { "total": 13, "valid": 13, "rank": 17 } },
- "wp:axiomatics": { "mult": { "lemma_sizeof_uint64_t_ok": { "qed": { "total": 1,
- "valid": 1 },
- "wp:main":
- { "total": 1,
- "valid": 1 } },
- "lemma_sizeof_uint32_t_ok": { "qed": { "total": 1,
- "valid": 1 },
- "wp:main":
- { "total": 1,
- "valid": 1 } },
- "wp:section": { "qed": { "total": 2,
- "valid": 2 },
- "wp:main": { "total": 2,
- "valid": 2 } } } },
+ "wp:main": { "total": 14, "valid": 14 } },
+ "wp:axiomatics": { "mult": { "lemma_sizeof_ok_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } } },
"wp:functions": { "BinaryMultiplication": { "BinaryMultiplication_assert_rte_unsigned_overflow_4":
- { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 6 },
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 6 } },
+ "valid": 1 } },
"BinaryMultiplication_assert_rte_unsigned_overflow_3":
- { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 6 },
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 6 } },
+ "valid": 1 } },
"BinaryMultiplication_assert_rte_unsigned_overflow_2":
- { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 10 },
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 10 } },
+ "valid": 1 } },
"BinaryMultiplication_assert_rte_unsigned_overflow":
- { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 5 },
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 5 } },
+ "valid": 1 } },
"BinaryMultiplication_loop_invariant_inv2_ok_deductible":
- { "alt-ergo": { "total": 2,
- "valid": 2,
- "rank": 10 },
+ { "why3:alt-ergo": { "total": 2,
+ "valid": 2 },
"wp:main": { "total": 2,
- "valid": 2,
- "rank": 10 } },
+ "valid": 2 } },
+ "BinaryMultiplication_loop_invariant_inv1_ok":
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
"BinaryMultiplication_assert_a1_ok_deductible":
- { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 3 },
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 3 } },
+ "valid": 1 } },
"BinaryMultiplication_loop_variant":
- { "alt-ergo": { "total": 2,
- "valid": 2,
- "rank": 8 },
+ { "why3:alt-ergo": { "total": 2,
+ "valid": 2 },
"wp:main": { "total": 2,
- "valid": 2,
- "rank": 8 } },
+ "valid": 2 } },
"BinaryMultiplication_loop_assigns":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"BinaryMultiplication_ensures_product":
- { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 16 },
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 16 } },
- "wp:section": { "alt-ergo":
- { "total": 10,
- "valid": 10,
- "rank": 17 },
+ "valid": 1 } },
+ "wp:section": { "why3:alt-ergo":
+ { "total": 11,
+ "valid": 11 },
"qed":
- { "total": 1,
- "valid": 1 },
+ { "total": 2,
+ "valid": 2 },
"wp:main":
- { "total": 11,
- "valid": 11,
- "rank": 17 } } } } }
+ { "total": 13,
+ "valid": 13 } } } } }
diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
index 08906aa5f7371a840eb06784a350d35311a40360..11732fd2cf5d647e279f21c7898b93f5d3fa6d7e 100644
--- a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
+++ b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
@@ -3,34 +3,33 @@
*/
/* run.config_qualif
- OPT: -wp-prop=-lack -then -wp-rte -wp -wp-prop=-lack
+ OPT: -wp-prover why3:alt-ergo -wp-prop=-lack -then -wp-rte -wp -wp-prop=-lack
*/
typedef unsigned uint32_t ;
typedef unsigned long long uint64_t ;
/*@ axiomatic mult {
- @ lemma sizeof_uint32_t: ok: sizeof(uint32_t) == 4; // 4 bytes: 32 bits
- @ lemma sizeof_uint64_t: ok: sizeof(uint64_t) == 8; // 8 bytes: 64 bits
- @
- @ lemma ax1: lack: \forall integer x, y; 0<=x && 0< y ==> 0 <= x <= x*y;
- @ lemma ax2: lack: \forall integer x, y; 0<=x && 0<=y ==> 0 <= 2*x*(y/2) <= x*y;
- @ lemma ax3: lack: \forall integer x, y; (uint64_t)(x * ((uint64_t)y)) == (uint64_t)(x*y) ;
- @ lemma ax4: lack: \forall integer x, y; (uint64_t)(x + ((uint64_t)y)) == (uint64_t)(x+y) ;
- @ lemma ax5: ok: \forall integer x, y; (uint64_t)(((uint64_t)x) * y) == (uint64_t)(x*y) ;
- @ lemma ax6: ok: \forall integer x, y; (uint64_t)(((uint64_t)x) + y) == (uint64_t)(x+y) ;
+ @ lemma sizeof_ok: ok: sizeof(uint64_t) == 2*sizeof(uint32_t);
+
+ @ lemma ax1: lack: \forall integer x, y; 0<x && 0<y ==> 0 <= 2*x*(y/2) <= x*y;
+
+ @ lemma ax2: lack: \forall integer x, y; (uint64_t)(x * ((uint64_t)y)) == (uint64_t)(x*y) ;
+ @ lemma ax3: lack: \forall integer x, y; (uint64_t)(x + ((uint64_t)y)) == (uint64_t)(x+y) ;
+ @ lemma ax4: ok: \forall integer x, y; (uint64_t)(((uint64_t)x) * y) == (uint64_t)(x*y) ;
+ @ lemma ax5: ok: \forall integer x, y; (uint64_t)(((uint64_t)x) + y) == (uint64_t)(x+y) ;
@ }
@ */
//@ ensures product: \result == a*b;
uint64_t BinaryMultiplication (uint32_t a, uint32_t b) {
- //@ assert a1: ok: deductible: a*b <= 18446744073709551615; // deductible from type size
+ //@ assert a1: ok: deductible: a*b <= 18446744073709551615; // deductible from size of C types
uint64_t r=0;
uint64_t x=a;
if (b != 0) {
/*@ loop assigns r, x, b;
- @ loop invariant inv1: lack: r+x*b == \at(a*b, LoopEntry);
- @ loop invariant inv2: lack: r+x == (uint64_t)(r+x);
+ @ loop invariant inv1: ok: r+x*b == \at(a*b, LoopEntry);
+ @ loop invariant inv2: ok: deductible: 2*x*(b/2) <= 18446744073709551615; // deductible from inv1, ax1, a1 and x>=0, b>0, r>=0
@ loop variant ok: b ;
@*/
while (1) {
diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c.0.report.json b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c.0.report.json
index c033820912ee4cc581d52e26d70abe6b30d842df..1323c0ee776d77f1effe6fb3a814c5a81632a111 100644
--- a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c.0.report.json
+++ b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c.0.report.json
@@ -1,84 +1,72 @@
-{ "wp:global": { "alt-ergo": { "total": 8, "valid": 8, "rank": 34 },
+{ "wp:global": { "why3:alt-ergo": { "total": 11, "valid": 11 },
"qed": { "total": 3, "valid": 3 },
- "wp:main": { "total": 11, "valid": 11, "rank": 34 } },
- "wp:axiomatics": { "mult": { "lemma_sizeof_uint64_t_ok": { "qed": { "total": 1,
+ "wp:main": { "total": 14, "valid": 14 } },
+ "wp:axiomatics": { "mult": { "lemma_sizeof_ok_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "lemma_ax5_ok": { "why3:alt-ergo": { "total": 1,
"valid": 1 },
- "wp:main":
- { "total": 1,
- "valid": 1 } },
- "lemma_sizeof_uint32_t_ok": { "qed": { "total": 1,
- "valid": 1 },
- "wp:main":
- { "total": 1,
- "valid": 1 } },
- "lemma_ax6_ok": { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 1 } },
- "lemma_ax5_ok": { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 1 },
+ "valid": 1 } },
+ "lemma_ax4_ok": { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 1 } },
- "wp:section": { "alt-ergo": { "total": 2,
- "valid": 2,
- "rank": 1 },
- "qed": { "total": 2,
- "valid": 2 },
- "wp:main": { "total": 4,
- "valid": 4,
- "rank": 1 } } } },
+ "valid": 1 } },
+ "wp:section": { "why3:alt-ergo": { "total": 2,
+ "valid": 2 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 3,
+ "valid": 3 } } } },
"wp:functions": { "BinaryMultiplication": { "BinaryMultiplication_assert_a3_ok":
- { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 14 },
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 14 } },
+ "valid": 1 } },
"BinaryMultiplication_assert_a2_ok":
- { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 12 },
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 12 } },
+ "valid": 1 } },
+ "BinaryMultiplication_loop_invariant_inv2_ok_deductible":
+ { "why3:alt-ergo": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "BinaryMultiplication_loop_invariant_inv1_ok":
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
"BinaryMultiplication_assert_a1_ok_deductible":
- { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 3 },
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 3 } },
+ "valid": 1 } },
"BinaryMultiplication_loop_variant":
- { "alt-ergo": { "total": 2,
- "valid": 2,
- "rank": 19 },
+ { "why3:alt-ergo": { "total": 2,
+ "valid": 2 },
"wp:main": { "total": 2,
- "valid": 2,
- "rank": 19 } },
+ "valid": 2 } },
"BinaryMultiplication_loop_assigns":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"BinaryMultiplication_ensures_product":
- { "alt-ergo": { "total": 1,
- "valid": 1,
- "rank": 34 },
+ { "why3:alt-ergo": { "total": 1,
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 34 } },
- "wp:section": { "alt-ergo":
- { "total": 6,
- "valid": 6,
- "rank": 34 },
+ "valid": 1 } },
+ "wp:section": { "why3:alt-ergo":
+ { "total": 9,
+ "valid": 9 },
"qed":
- { "total": 1,
- "valid": 1 },
+ { "total": 2,
+ "valid": 2 },
"wp:main":
- { "total": 7,
- "valid": 7,
- "rank": 34 } } } } }
+ { "total": 11,
+ "valid": 11 } } } } }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
index 5b136a7658cd0354170f2f4419e8b46fc2ab56bf..1274212b3de4edfa6b92d981a76d07bae8da56e8 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
@@ -4,13 +4,11 @@
[wp] Loading driver 'share/wp.driver'
[rte] annotating function BinaryMultiplication
[wp] Goal typed_lemma_ax1_lack : not tried
-[wp] Goal typed_lemma_ax2_lack : not tried
-[wp] Goal typed_lemma_sizeof_uint32_t_ok : trivial
-[wp] Goal typed_lemma_sizeof_uint64_t_ok : trivial
+[wp] Goal typed_lemma_sizeof_ok_ok : trivial
[wp] Goal typed_BinaryMultiplication_ensures_product : not tried
[wp] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : not tried
-[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_lack_preserved : not tried
-[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_lack_established : not tried
+[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : not tried
+[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : not tried
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_preserved : not tried
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : not tried
[wp] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle
index d37e8c31f601efd5331dd29b2cd443a53cf41528..6473cd6ed5f76aec602b64c92c388b3f294a6c93 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle
@@ -6,17 +6,15 @@
[wp] Goal typed_lemma_ax1_lack : not tried
[wp] Goal typed_lemma_ax2_lack : not tried
[wp] Goal typed_lemma_ax3_lack : not tried
-[wp] Goal typed_lemma_ax4_lack : not tried
+[wp] Goal typed_lemma_ax4_ok : not tried
[wp] Goal typed_lemma_ax5_ok : not tried
-[wp] Goal typed_lemma_ax6_ok : not tried
-[wp] Goal typed_lemma_sizeof_uint32_t_ok : trivial
-[wp] Goal typed_lemma_sizeof_uint64_t_ok : trivial
+[wp] Goal typed_lemma_sizeof_ok_ok : trivial
[wp] Goal typed_BinaryMultiplication_ensures_product : not tried
[wp] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : not tried
-[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_lack_preserved : not tried
-[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_lack_established : not tried
-[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_lack_preserved : not tried
-[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_lack_established : not tried
+[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : not tried
+[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : not tried
+[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_preserved : not tried
+[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : not tried
[wp] Goal typed_BinaryMultiplication_assert_a2_ok : not tried
[wp] Goal typed_BinaryMultiplication_assert_a3_ok : not tried
[wp] Goal typed_BinaryMultiplication_loop_assigns : trivial
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 9ff5c4e14638d08ecbd7961498b5e8d1016a00c4..54c0e393099c80318ef0b908639542e56799eef3 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
@@ -3,51 +3,53 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 9 goals scheduled
-[wp] [Qed] Goal typed_lemma_sizeof_uint32_t_ok : Valid
-[wp] [Qed] Goal typed_lemma_sizeof_uint64_t_ok : 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_loop_invariant_inv2_ok_deductible_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : Valid
+[wp] 10 goals scheduled
+[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : 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_loop_invariant_inv1_ok_preserved : Valid
+[wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_preserved : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : 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_positive : Valid
-[wp] Proved goals: 9 / 9
+[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: 6
+ alt-ergo: 7
[wp] Report 'tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
-Axiomatic mult 2 - 2 100%
+Axiomatic mult 1 - 1 100%
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-BinaryMultiplication 1 6 (64..88) 7 100%
+BinaryMultiplication 2 - 9 100%
-------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function BinaryMultiplication
-[wp] 13 goals scheduled
-[wp] [Qed] Goal typed_lemma_sizeof_uint32_t_ok : Valid
-[wp] [Qed] Goal typed_lemma_sizeof_uint64_t_ok : 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_loop_invariant_inv2_ok_deductible_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_2 : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_3 : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_4 : Valid
+[wp] 14 goals scheduled
+[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : 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_loop_invariant_inv1_ok_preserved : Valid
+[wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_preserved : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_2 : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_3 : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_4 : 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_positive : Valid
-[wp] Proved goals: 10 / 13
+[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: 10
+ alt-ergo: 11
[wp] Report 'tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
-Axiomatic mult 2 - 2 100%
+Axiomatic mult 1 - 1 100%
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-BinaryMultiplication 1 10 (64..88) 11 100%
+BinaryMultiplication 2 - 13 100%
-------------------------------------------------------------
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 4ed3a30466c56941d1f80920b99c2a74bf8b43bd..dd5a5577e64cd94e04a81eac8f0df4277d82c64b 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
@@ -3,51 +3,57 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 11 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_ax5_ok : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_ax6_ok : Valid
-[wp] [Qed] Goal typed_lemma_sizeof_uint32_t_ok : Valid
-[wp] [Qed] Goal typed_lemma_sizeof_uint64_t_ok : 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_a2_ok : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a3_ok : Valid
+[wp] 14 goals scheduled
+[wp] [alt-ergo] Goal typed_lemma_ax4_ok : Valid
+[wp] [alt-ergo] Goal typed_lemma_ax5_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_assert_a1_ok_deductible : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Valid
+[wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_preserved : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_assert_a2_ok : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_assert_a3_ok : 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_positive : Valid
-[wp] Proved goals: 11 / 11
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
+[wp] Proved goals: 14 / 14
Qed: 3
- Alt-Ergo: 8
+ alt-ergo: 11
[wp] Report 'tests/wp_gallery/binary-multiplication.c.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
-Axiomatic mult 2 2 (1..12) 4 100%
+Axiomatic mult 1 - 3 100%
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-BinaryMultiplication 1 6 (208..256) 7 100%
+BinaryMultiplication 2 - 11 100%
-------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function BinaryMultiplication
-[wp] 11 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_ax5_ok : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_ax6_ok : Valid
-[wp] [Qed] Goal typed_lemma_sizeof_uint32_t_ok : Valid
-[wp] [Qed] Goal typed_lemma_sizeof_uint64_t_ok : 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_a2_ok : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a3_ok : Valid
+[wp] 14 goals scheduled
+[wp] [alt-ergo] Goal typed_lemma_ax4_ok : Valid
+[wp] [alt-ergo] Goal typed_lemma_ax5_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_assert_a1_ok_deductible : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Valid
+[wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_preserved : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_assert_a2_ok : Valid
+[wp] [alt-ergo] Goal typed_BinaryMultiplication_assert_a3_ok : 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_positive : Valid
-[wp] Proved goals: 8 / 11
+[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: 8
+ alt-ergo: 11
[wp] Report 'tests/wp_gallery/binary-multiplication.c.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
-Axiomatic mult 2 2 (1..12) 4 100%
+Axiomatic mult 1 - 3 100%
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-BinaryMultiplication 1 6 (208..256) 7 100%
+BinaryMultiplication 2 - 11 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json b/src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json
index c36b874055fa6135a97ad7aadb2b4b37f77cca50..07e8025452aa4ebb4c03c254c4bdca0be3e21646 100644
--- a/src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json
+++ b/src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json
@@ -36,12 +36,12 @@
"memcpy_loop_assigns": { "alt-ergo":
{ "total": 1,
"valid": 1,
- "rank": 40 },
+ "rank": 43 },
"qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 3,
"valid": 3,
- "rank": 40 } },
+ "rank": 43 } },
"memcpy_ensures_result_ptr": { "qed":
{ "total": 1,
"valid": 1 },