Skip to content
Snippets Groups Projects
Commit b2eb4213 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[wp] some more tests

parent a1fb64ff
No related branches found
No related tags found
No related merge requests found
......@@ -138,5 +138,9 @@ unsigned char cast_uchar(int x) {
//@ check bit_set_unset2: ok: (c & 0x77) == 0x66 && (x & 5) == (x & 7) ==> (P(x & 4) <==> P(x & 6)) ;
//@ check bit_defined: ok: (c & 0x77) == 0x66 && (x & ~0x77) == (~0x77 & 0xFFF0) ==> (P(c)<==>P(0xE6));
//@ check bit_defined2: ok: (c & 0x77) == 0x66 && (x & ~0x77) == (~0x77 & 0xFFF0) ==> (P(x)<==>P(0xFFE6));
//@ check bit_to_signed_positive: ok: (x & 0xFF) == 0x60 ==> (P((signed char) x) <==> P(0x60));
//@ check bit_to_signed_positive2: ok: (x & 0xF0) == 0x60 ==> (((signed char) x) & (1 << 10)) == 0;
//@ check bit_to_signed_negative: ok: (x & 0xFF) == 0x86 ==> (P((signed char) x) <==> P(0x86|~255));
//@ check bit_to_signed_negative2: ok: (x & 0xF0) == 0x80 ==> (((signed char) x) & (1 << 10)) != 0;
return c;
}
......@@ -255,6 +255,26 @@ Prove: true.
Goal Check 'bit_defined2,ok' (file bitwise.i, line 140):
Prove: true.
------------------------------------------------------------
Goal Check 'bit_to_signed_positive,ok' (file bitwise.i, line 141):
Prove: true.
------------------------------------------------------------
Goal Check 'bit_to_signed_positive2,ok' (file bitwise.i, line 142):
Prove: true.
------------------------------------------------------------
Goal Check 'bit_to_signed_negative,ok' (file bitwise.i, line 143):
Prove: true.
------------------------------------------------------------
Goal Check 'bit_to_signed_negative2,ok' (file bitwise.i, line 144):
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function lemma
......
......@@ -2,7 +2,7 @@
[kernel] Parsing bitwise.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 45 goals scheduled
[wp] 49 goals scheduled
[wp] [Qed] Goal typed_band_ensures : Valid
[wp] [Qed] Goal typed_band_ensures_band0 : Valid
[wp] [Qed] Goal typed_band_bit0_ensures_band1 : Valid
......@@ -48,8 +48,12 @@
[wp] [Qed] Goal typed_cast_uchar_check_bit_set_unset2_ok : Valid
[wp] [Qed] Goal typed_cast_uchar_check_bit_defined_ok : Valid
[wp] [Qed] Goal typed_cast_uchar_check_bit_defined2_ok : Valid
[wp] Proved goals: 45 / 45
Qed: 42
[wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_positive_ok : Valid
[wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_positive2_ok : Valid
[wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_negative_ok : Valid
[wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_negative2_ok : Valid
[wp] Proved goals: 49 / 49
Qed: 46
Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......@@ -63,5 +67,5 @@
band_bool 1 1 2 100%
bxor_bool 1 1 2 100%
lemma 7 - 7 100%
cast_uchar 8 - 8 100%
cast_uchar 12 - 12 100%
------------------------------------------------------------
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment