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

[Wp] improve bitwise simplifier: oracle upfdate

parent 230ead64
No related branches found
No related tags found
No related merge requests found
......@@ -2,7 +2,7 @@
[kernel] Parsing bitwise.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 49 goals scheduled
[wp] 51 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
......@@ -52,8 +52,10 @@
[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
[wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_ok : Valid
[wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed2_ok : Valid
[wp] Proved goals: 51 / 51
Qed: 48
Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......@@ -67,5 +69,5 @@
band_bool 1 1 2 100%
bxor_bool 1 1 2 100%
lemma 7 - 7 100%
cast_uchar 12 - 12 100%
cast_uchar 14 - 14 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