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

Merge branch 'feature/patrick/wp-gallery' into 'master' 

Multiplication Russe (ou binaire)

See merge request frama-c/frama-c!2140
parents 384e2618 80fbae00
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 198 additions and 225 deletions
src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c
+ 8
− 9
View file @ 250e6a8a
...@@ -3,30 +3,29 @@ ...@@ -3,30 +3,29 @@
*/ */
/* run.config_qualif /* 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 uint32_t ;
typedef unsigned long long uint64_t ; typedef unsigned long long uint64_t ;
/*@ axiomatic mult { /*@ 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 sizeof_ok: ok: sizeof(uint64_t) == 2 * sizeof(uint32_t);
@
@ lemma ax1: lack: \forall integer x, y; 0<=x && 0< y ==> 0 <= x <= x*y; @ 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; 0<=x && 0<=y ==> 0 <= 2*x*(y/2) <= x*y;
@ } @ }
@ */ @ */
//@ ensures product: \result == a*b; //@ ensures product: \result == a*b;
uint64_t BinaryMultiplication (uint32_t a, uint32_t 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 r=0;
uint64_t x=a; uint64_t x=a;
if (b != 0) { if (b != 0) {
/*@ loop assigns ok: r, x, b; /*@ loop assigns ok: r, x, b;
@ loop invariant inv1: lack: r+x*b == \at(a*b, LoopEntry); @ loop invariant inv1: ok: 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 inv2: ok: deductible: 2*x*(b/2) <= 18446744073709551615; // deductible from inv1, ax1, a1 and x>=0, b>0, r>=0
@ loop variant ok: b ; @ loop variant ok: b ;
@*/ @*/
while (1) { while (1) {
......
src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json
+ 48
− 65
View file @ 250e6a8a
{ "wp:global": { "alt-ergo": { "total": 10, "valid": 10, "rank": 17 }, { "wp:global": { "why3:alt-ergo": { "total": 11, "valid": 11 },
"qed": { "total": 3, "valid": 3 }, "qed": { "total": 3, "valid": 3 },
"wp:main": { "total": 13, "valid": 13, "rank": 17 } }, "wp:main": { "total": 14, "valid": 14 } },
"wp:axiomatics": { "mult": { "lemma_sizeof_uint64_t_ok": { "qed": { "total": 1, "wp:axiomatics": { "mult": { "lemma_sizeof_ok_ok": { "qed": { "total": 1,
"valid": 1 }, "valid": 1 },
"wp:main": "wp:main": { "total": 1,
{ "total": 1, "valid": 1 } },
"valid": 1 } }, "wp:section": { "qed": { "total": 1,
"lemma_sizeof_uint32_t_ok": { "qed": { "total": 1, "valid": 1 },
"valid": 1 }, "wp:main": { "total": 1,
"wp:main": "valid": 1 } } } },
{ "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } } } },
"wp:functions": { "BinaryMultiplication": { "BinaryMultiplication_assert_rte_unsigned_overflow_4": "wp:functions": { "BinaryMultiplication": { "BinaryMultiplication_assert_rte_unsigned_overflow_4":
{ "alt-ergo": { "total": 1, { "why3:alt-ergo": { "total": 1,
"valid": 1, "valid": 1 },
"rank": 6 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 6 } },
"BinaryMultiplication_assert_rte_unsigned_overflow_3": "BinaryMultiplication_assert_rte_unsigned_overflow_3":
{ "alt-ergo": { "total": 1, { "why3:alt-ergo": { "total": 1,
"valid": 1, "valid": 1 },
"rank": 6 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 6 } },
"BinaryMultiplication_assert_rte_unsigned_overflow_2": "BinaryMultiplication_assert_rte_unsigned_overflow_2":
{ "alt-ergo": { "total": 1, { "why3:alt-ergo": { "total": 1,
"valid": 1, "valid": 1 },
"rank": 10 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 10 } },
"BinaryMultiplication_assert_rte_unsigned_overflow": "BinaryMultiplication_assert_rte_unsigned_overflow":
{ "alt-ergo": { "total": 1, { "why3:alt-ergo": { "total": 1,
"valid": 1, "valid": 1 },
"rank": 5 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 5 } },
"BinaryMultiplication_loop_invariant_inv2_ok_deductible": "BinaryMultiplication_loop_invariant_inv2_ok_deductible":
{ "alt-ergo": { "total": 2, { "why3:alt-ergo": { "total": 2,
"valid": 2, "valid": 2 },
"rank": 10 },
"wp:main": { "total": 2, "wp:main": { "total": 2,
"valid": 2, "valid": 2 } },
"rank": 10 } }, "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": "BinaryMultiplication_assert_a1_ok_deductible":
{ "alt-ergo": { "total": 1, { "why3:alt-ergo": { "total": 1,
"valid": 1, "valid": 1 },
"rank": 3 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 3 } },
"BinaryMultiplication_loop_variant": "BinaryMultiplication_loop_variant":
{ "alt-ergo": { "total": 2, { "why3:alt-ergo": { "total": 2,
"valid": 2, "valid": 2 },
"rank": 8 },
"wp:main": { "total": 2, "wp:main": { "total": 2,
"valid": 2, "valid": 2 } },
"rank": 8 } },
"BinaryMultiplication_loop_assigns": "BinaryMultiplication_loop_assigns":
{ "qed": { "total": 1, { "qed": { "total": 1,
"valid": 1 }, "valid": 1 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1 } }, "valid": 1 } },
"BinaryMultiplication_ensures_product": "BinaryMultiplication_ensures_product":
{ "alt-ergo": { "total": 1, { "why3:alt-ergo": { "total": 1,
"valid": 1, "valid": 1 },
"rank": 16 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 16 } }, "wp:section": { "why3:alt-ergo":
"wp:section": { "alt-ergo": { "total": 11,
{ "total": 10, "valid": 11 },
"valid": 10,
"rank": 17 },
"qed": "qed":
{ "total": 1, { "total": 2,
"valid": 1 }, "valid": 2 },
"wp:main": "wp:main":
{ "total": 11, { "total": 13,
"valid": 11, "valid": 13 } } } } }
"rank": 17 } } } } }
src/plugins/wp/tests/wp_gallery/binary-multiplication.c
+ 12
− 13
View file @ 250e6a8a
...@@ -3,34 +3,33 @@ ...@@ -3,34 +3,33 @@
*/ */
/* run.config_qualif /* 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 uint32_t ;
typedef unsigned long long uint64_t ; typedef unsigned long long uint64_t ;
/*@ axiomatic mult { /*@ axiomatic mult {
@ lemma sizeof_uint32_t: ok: sizeof(uint32_t) == 4; // 4 bytes: 32 bits @ lemma sizeof_ok: ok: sizeof(uint64_t) == 2*sizeof(uint32_t);
@ 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 <= 2*x*(y/2) <= x*y;
@ 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 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 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 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) ; @ 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) ;
@ } @ }
@ */ @ */
//@ ensures product: \result == a*b; //@ ensures product: \result == a*b;
uint64_t BinaryMultiplication (uint32_t a, uint32_t 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 r=0;
uint64_t x=a; uint64_t x=a;
if (b != 0) { if (b != 0) {
/*@ loop assigns r, x, b; /*@ loop assigns r, x, b;
@ loop invariant inv1: lack: r+x*b == \at(a*b, LoopEntry); @ loop invariant inv1: ok: r+x*b == \at(a*b, LoopEntry);
@ loop invariant inv2: lack: r+x == (uint64_t)(r+x); @ 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 ; @ loop variant ok: b ;
@*/ @*/
while (1) { while (1) {
......
src/plugins/wp/tests/wp_gallery/binary-multiplication.c.0.report.json
+ 51
− 63
View file @ 250e6a8a
{ "wp:global": { "alt-ergo": { "total": 8, "valid": 8, "rank": 34 }, { "wp:global": { "why3:alt-ergo": { "total": 11, "valid": 11 },
"qed": { "total": 3, "valid": 3 }, "qed": { "total": 3, "valid": 3 },
"wp:main": { "total": 11, "valid": 11, "rank": 34 } }, "wp:main": { "total": 14, "valid": 14 } },
"wp:axiomatics": { "mult": { "lemma_sizeof_uint64_t_ok": { "qed": { "total": 1, "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 }, "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, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 1 } }, "lemma_ax4_ok": { "why3:alt-ergo": { "total": 1,
"lemma_ax5_ok": { "alt-ergo": { "total": 1, "valid": 1 },
"valid": 1,
"rank": 1 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 1 } }, "wp:section": { "why3:alt-ergo": { "total": 2,
"wp:section": { "alt-ergo": { "total": 2, "valid": 2 },
"valid": 2, "qed": { "total": 1,
"rank": 1 }, "valid": 1 },
"qed": { "total": 2, "wp:main": { "total": 3,
"valid": 2 }, "valid": 3 } } } },
"wp:main": { "total": 4,
"valid": 4,
"rank": 1 } } } },
"wp:functions": { "BinaryMultiplication": { "BinaryMultiplication_assert_a3_ok": "wp:functions": { "BinaryMultiplication": { "BinaryMultiplication_assert_a3_ok":
{ "alt-ergo": { "total": 1, { "why3:alt-ergo": { "total": 1,
"valid": 1, "valid": 1 },
"rank": 14 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 14 } },
"BinaryMultiplication_assert_a2_ok": "BinaryMultiplication_assert_a2_ok":
{ "alt-ergo": { "total": 1, { "why3:alt-ergo": { "total": 1,
"valid": 1, "valid": 1 },
"rank": 12 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 12 } }, "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": "BinaryMultiplication_assert_a1_ok_deductible":
{ "alt-ergo": { "total": 1, { "why3:alt-ergo": { "total": 1,
"valid": 1, "valid": 1 },
"rank": 3 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 3 } },
"BinaryMultiplication_loop_variant": "BinaryMultiplication_loop_variant":
{ "alt-ergo": { "total": 2, { "why3:alt-ergo": { "total": 2,
"valid": 2, "valid": 2 },
"rank": 19 },
"wp:main": { "total": 2, "wp:main": { "total": 2,
"valid": 2, "valid": 2 } },
"rank": 19 } },
"BinaryMultiplication_loop_assigns": "BinaryMultiplication_loop_assigns":
{ "qed": { "total": 1, { "qed": { "total": 1,
"valid": 1 }, "valid": 1 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1 } }, "valid": 1 } },
"BinaryMultiplication_ensures_product": "BinaryMultiplication_ensures_product":
{ "alt-ergo": { "total": 1, { "why3:alt-ergo": { "total": 1,
"valid": 1, "valid": 1 },
"rank": 34 },
"wp:main": { "total": 1, "wp:main": { "total": 1,
"valid": 1, "valid": 1 } },
"rank": 34 } }, "wp:section": { "why3:alt-ergo":
"wp:section": { "alt-ergo": { "total": 9,
{ "total": 6, "valid": 9 },
"valid": 6,
"rank": 34 },
"qed": "qed":
{ "total": 1, { "total": 2,
"valid": 1 }, "valid": 2 },
"wp:main": "wp:main":
{ "total": 7, { "total": 11,
"valid": 7, "valid": 11 } } } } }
"rank": 34 } } } } }
src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
+ 3
− 5
View file @ 250e6a8a
...@@ -4,13 +4,11 @@ ...@@ -4,13 +4,11 @@
[wp] Loading driver 'share/wp.driver' [wp] Loading driver 'share/wp.driver'
[rte] annotating function BinaryMultiplication [rte] annotating function BinaryMultiplication
[wp] Goal typed_lemma_ax1_lack : not tried [wp] Goal typed_lemma_ax1_lack : not tried
[wp] Goal typed_lemma_ax2_lack : not tried [wp] Goal typed_lemma_sizeof_ok_ok : trivial
[wp] Goal typed_lemma_sizeof_uint32_t_ok : trivial
[wp] Goal typed_lemma_sizeof_uint64_t_ok : trivial
[wp] Goal typed_BinaryMultiplication_ensures_product : not tried [wp] Goal typed_BinaryMultiplication_ensures_product : not tried
[wp] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : 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_ok_preserved : not tried
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_lack_established : 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_preserved : not tried
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : not tried [wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : not tried
[wp] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow : not tried [wp] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow : not tried
......
src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle
+ 6
− 8
View file @ 250e6a8a
...@@ -6,17 +6,15 @@ ...@@ -6,17 +6,15 @@
[wp] Goal typed_lemma_ax1_lack : not tried [wp] Goal typed_lemma_ax1_lack : not tried
[wp] Goal typed_lemma_ax2_lack : not tried [wp] Goal typed_lemma_ax2_lack : not tried
[wp] Goal typed_lemma_ax3_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_ax5_ok : not tried
[wp] Goal typed_lemma_ax6_ok : not tried [wp] Goal typed_lemma_sizeof_ok_ok : trivial
[wp] Goal typed_lemma_sizeof_uint32_t_ok : trivial
[wp] Goal typed_lemma_sizeof_uint64_t_ok : trivial
[wp] Goal typed_BinaryMultiplication_ensures_product : not tried [wp] Goal typed_BinaryMultiplication_ensures_product : not tried
[wp] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : 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_ok_preserved : not tried
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_lack_established : not tried [wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : not tried
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_lack_preserved : not tried [wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_preserved : not tried
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_lack_established : 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_a2_ok : not tried
[wp] Goal typed_BinaryMultiplication_assert_a3_ok : not tried [wp] Goal typed_BinaryMultiplication_assert_a3_ok : not tried
[wp] Goal typed_BinaryMultiplication_loop_assigns : trivial [wp] Goal typed_BinaryMultiplication_loop_assigns : trivial
......
src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+ 32
− 30
View file @ 250e6a8a
...@@ -3,51 +3,53 @@ ...@@ -3,51 +3,53 @@
[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] 9 goals scheduled [wp] 10 goals scheduled
[wp] [Qed] Goal typed_lemma_sizeof_uint32_t_ok : Valid [wp] [Qed] Goal typed_lemma_sizeof_ok_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_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_inv2_ok_deductible_preserved : Valid [wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_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] [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: 9 / 9 [wp] Proved goals: 10 / 10
Qed: 3 Qed: 3
Alt-Ergo: 6 alt-ergo: 7
[wp] Report 'tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json' [wp] Report 'tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success Axiomatics WP Alt-Ergo Total Success
Axiomatic mult 2 - 2 100% Axiomatic mult 1 - 1 100%
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
BinaryMultiplication 1 6 (64..88) 7 100% BinaryMultiplication 2 - 9 100%
------------------------------------------------------------- -------------------------------------------------------------
[wp] Running WP plugin... [wp] Running WP plugin...
[rte] annotating function BinaryMultiplication [rte] annotating function BinaryMultiplication
[wp] 13 goals scheduled [wp] 14 goals scheduled
[wp] [Qed] Goal typed_lemma_sizeof_uint32_t_ok : Valid [wp] [Qed] Goal typed_lemma_sizeof_ok_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_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_inv2_ok_deductible_preserved : Valid [wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : Valid [wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_preserved : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow : Valid [wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_2 : Valid [wp] [alt-ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_3 : Valid [wp] [alt-ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_2 : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_4 : 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] [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: 10 / 13 [wp] Proved goals: 11 / 14
Qed: 0 Qed: 0
Alt-Ergo: 10 alt-ergo: 11
[wp] Report 'tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json' [wp] Report 'tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success Axiomatics WP Alt-Ergo Total Success
Axiomatic mult 2 - 2 100% Axiomatic mult 1 - 1 100%
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
BinaryMultiplication 1 10 (64..88) 11 100% BinaryMultiplication 2 - 13 100%
------------------------------------------------------------- -------------------------------------------------------------
src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+ 36
− 30
View file @ 250e6a8a
...@@ -3,51 +3,57 @@ ...@@ -3,51 +3,57 @@
[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] 11 goals scheduled [wp] 14 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ax5_ok : Valid [wp] [alt-ergo] Goal typed_lemma_ax4_ok : Valid
[wp] [Alt-Ergo] Goal typed_lemma_ax6_ok : Valid [wp] [alt-ergo] Goal typed_lemma_ax5_ok : Valid
[wp] [Qed] Goal typed_lemma_sizeof_uint32_t_ok : Valid [wp] [Qed] Goal typed_lemma_sizeof_ok_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_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_assert_a2_ok : Valid [wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a3_ok : 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] [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: 11 / 11 [wp] Proved goals: 14 / 14
Qed: 3 Qed: 3
Alt-Ergo: 8 alt-ergo: 11
[wp] Report 'tests/wp_gallery/binary-multiplication.c.0.report.json' [wp] Report 'tests/wp_gallery/binary-multiplication.c.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success 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 Functions WP Alt-Ergo Total Success
BinaryMultiplication 1 6 (208..256) 7 100% BinaryMultiplication 2 - 11 100%
------------------------------------------------------------- -------------------------------------------------------------
[wp] Running WP plugin... [wp] Running WP plugin...
[rte] annotating function BinaryMultiplication [rte] annotating function BinaryMultiplication
[wp] 11 goals scheduled [wp] 14 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ax5_ok : Valid [wp] [alt-ergo] Goal typed_lemma_ax4_ok : Valid
[wp] [Alt-Ergo] Goal typed_lemma_ax6_ok : Valid [wp] [alt-ergo] Goal typed_lemma_ax5_ok : Valid
[wp] [Qed] Goal typed_lemma_sizeof_uint32_t_ok : Valid [wp] [Qed] Goal typed_lemma_sizeof_ok_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_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_assert_a2_ok : Valid [wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a3_ok : 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] [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: 8 / 11 [wp] Proved goals: 11 / 14
Qed: 0 Qed: 0
Alt-Ergo: 8 alt-ergo: 11
[wp] Report 'tests/wp_gallery/binary-multiplication.c.0.report.json' [wp] Report 'tests/wp_gallery/binary-multiplication.c.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success 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 Functions WP Alt-Ergo Total Success
BinaryMultiplication 1 6 (208..256) 7 100% BinaryMultiplication 2 - 11 100%
------------------------------------------------------------- -------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json
+ 2
− 2
View file @ 250e6a8a
...@@ -36,12 +36,12 @@ ...@@ -36,12 +36,12 @@
"memcpy_loop_assigns": { "alt-ergo": "memcpy_loop_assigns": { "alt-ergo":
{ "total": 1, { "total": 1,
"valid": 1, "valid": 1,
"rank": 40 }, "rank": 43 },
"qed": { "total": 2, "qed": { "total": 2,
"valid": 2 }, "valid": 2 },
"wp:main": { "total": 3, "wp:main": { "total": 3,
"valid": 3, "valid": 3,
"rank": 40 } }, "rank": 43 } },
"memcpy_ensures_result_ptr": { "qed": "memcpy_ensures_result_ptr": { "qed":
{ "total": 1, { "total": 1,
"valid": 1 }, "valid": 1 },
......
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