diff --git a/src/plugins/wp/tests/wp_acsl/bitwise.i b/src/plugins/wp/tests/wp_acsl/bitwise.i
index 293b36629048e38c95684eafac82fd3d2d73eb05..1e3506895a4a765901b9cdec4872a687bdb1c830 100644
--- a/src/plugins/wp/tests/wp_acsl/bitwise.i
+++ b/src/plugins/wp/tests/wp_acsl/bitwise.i
@@ -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;
}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
index 826320b4e0960315eb92e2d8b2c3fa2ed51e14e5..85396b9cddcd26761a29df07cb1fff6f43f96829 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
@@ -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
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 d7eaf03568eef922af74f9b86939989f8ca01073..1eb2d8e53928a8a268ddd53941f83df69495e7da 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] 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%
------------------------------------------------------------