From 93178e75f82530a2d46becef49b4c2970cacf107 Mon Sep 17 00:00:00 2001 From: Patrick Baudin <patrick.baudin@cea.fr> Date: Tue, 22 Feb 2022 16:24:02 +0100 Subject: [PATCH] [Wp] improve bitwise simplifier: oracle upfdate --- .../wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle index 1eb2d8e5392..c7e6e96a370 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle @@ -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% ------------------------------------------------------------ -- GitLab