diff --git a/src/plugins/wp/share/why3/frama_c_wp/cbits.mlw b/src/plugins/wp/share/why3/frama_c_wp/cbits.mlw
index 7207fa0d437dc4d4a9108a9fef93195c0f0350a9..2d609dc75fe99a131b3b4dde6ec364b406573f7e 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cbits.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cbits.mlw
@@ -57,6 +57,7 @@ theory Cbits
(** ** land identities *)
axiom land_idemp: forall x:int [land x x]. (land x x) = x
+ axiom land_idemp_bis: forall x y : int [land x (land x y)]. land x (land x y) = land x y
axiom land_0: forall x:int [land 0 x]. (land 0 x) = 0
axiom land_0bis: forall x:int [land x 0]. (land x 0) = 0
axiom land_1: forall x:int [land (-1) x]. (land (-1) x) = x
@@ -67,6 +68,7 @@ theory Cbits
(** ** lor identities *)
axiom lor_idemp: forall x:int [lor x x]. (lor x x) = x
+ axiom lor_idemp_bis: forall x y : int [lor x (lor x y)]. lor x (lor x y) = lor x y
axiom lor_1: forall x:int [lor (-1) x]. (lor (-1) x) = -1
axiom lor_1bis: forall x:int [lor x (-1)]. (lor x (-1)) = -1
axiom lor_0: forall x:int [lor 0 x]. (lor 0 x) = x
@@ -77,6 +79,7 @@ theory Cbits
(** ** lxor identities *)
axiom lxor_nilpotent: forall x:int [lxor x x]. (lxor x x) = 0
+ axiom lxor_nilpotent_bis: forall x y : int [lxor x (lxor x y)]. lxor x (lxor x y) = y
axiom lxor_1: forall x:int [lxor (-1) x]. (lxor (-1) x) = (lnot x)
axiom lxor_1bis: forall x:int [lxor x (-1)]. (lxor x (-1)) = (lnot x)
axiom lxor_0: forall x:int [lxor 0 x]. (lxor 0 x) = x
@@ -481,7 +484,7 @@ theory Cbits
lemma is_sint_land: forall n x y:int.
is_sint n x -> is_sint n y -> to_sint n (land x y) = land x y
lemma is_sint_lsr: forall n x y:int.
- 0<=y -> is_sint n x -> to_sint n (lsr x y) = lsr x y
+ 0<=y -> is_sint n x -> to_sint n (lsr x y) = lsr x y
lemma is_sint_lsl1_inf : forall n y:int.
0<=y<n -> to_sint n (lsl 1 y) = (lsl 1 y)
lemma is_sint_lsl1_sup : forall n y:int.
@@ -508,7 +511,7 @@ theory Cbits
is_sint8 x -> is_sint8 y -> to_sint8 (land x y) = land x y
axiom is_sint8_lsr: forall x y:int [to_sint8 (lsr x y)].
- 0<=y -> is_sint8 x -> to_sint8 (lsr x y) = lsr x y
+ 0<=y -> is_sint8 x -> to_sint8 (lsr x y) = lsr x y
axiom is_sint8_lsl1 :
lsl 1 7 = Cint.max_sint8
@@ -524,7 +527,7 @@ theory Cbits
is_sint16 x -> to_sint16 (lnot x) = lnot x
axiom is_sint16_lxor : forall x y:int [to_sint16 (lxor x y)].
- is_sint16 x -> is_sint16 y -> to_sint16 (lxor x y) = lxor x y
+ is_sint16 x -> is_sint16 y -> to_sint16 (lxor x y) = lxor x y
axiom is_sint16_lor : forall x y:int [to_sint16 (lor x y)].
is_sint16 x -> is_sint16 y -> to_sint16 (lor x y) = lor x y
@@ -549,7 +552,7 @@ theory Cbits
is_sint32 x -> to_sint32 (lnot x) = lnot x
axiom is_sint32_lxor : forall x y:int [to_sint32 (lxor x y)].
- is_sint32 x -> is_sint32 y -> to_sint32 (lxor x y) = lxor x y
+ is_sint32 x -> is_sint32 y -> to_sint32 (lxor x y) = lxor x y
axiom is_sint32_lor : forall x y:int [to_sint32(lor x y)].
is_sint32 x -> is_sint32 y -> to_sint32 (lor x y) = lor x y
diff --git a/src/plugins/wp/tests/wp_acsl/bitwise_idemp.i b/src/plugins/wp/tests/wp_acsl/bitwise_idemp.i
new file mode 100644
index 0000000000000000000000000000000000000000..61f3abf7668e4da1077013226d6a65f4dcdb8947
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/bitwise_idemp.i
@@ -0,0 +1,42 @@
+/*
+ X Y | X & Y | X & (X & Y)
+ | |
+ 0 0 | 0 | 0
+ 0 1 | 0 | 0
+ 1 0 | 0 | 0
+ 1 1 | 1 | 1
+*/
+
+void land(int x, int a, int b, int c, int d) {
+ //@ check A: (x ? c == a : c == b) ==> (a & (b & c)) == (a & b) ;
+ //@ check B: (x ? c == a : c == b) ==> ((a & b) & c) == (a & b) ;
+}
+
+/*
+ X Y | X | Y | X | (X | Y)
+ | |
+ 0 0 | 0 | 0
+ 0 1 | 1 | 1
+ 1 0 | 1 | 1
+ 1 1 | 1 | 1
+
+*/
+
+void lor(int x, int a, int b, int c, int d) {
+ //@ check A: (x ? c == a : c == b) ==> (a | (b | c)) == (a | b) ;
+ //@ check B: (x ? c == a : c == b) ==> ((a | b) | c) == (a | b) ;
+}
+
+/*
+ X Y | X ^ Y | X ^ (X ^ Y)
+ | |
+ 0 0 | 0 | 0
+ 0 1 | 1 | 1
+ 1 0 | 1 | 0
+ 1 1 | 0 | 1
+*/
+
+void lxor(int x, int a, int b, int c, int d, int e) {
+ //@ check A: (x ? c == a && e == b : c == b && e == a) ==> (a ^ (b ^ c)) == e ;
+ //@ check B: (x ? c == a && e == b : c == b && e == a) ==> ((a ^ b) ^ c) == e ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise_idemp.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise_idemp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f80dac5a4192881eb6bf83ff9ebee27388f759b8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise_idemp.res.oracle
@@ -0,0 +1,75 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/bitwise_idemp.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function land
+------------------------------------------------------------
+
+Goal Check 'A' (file tests/wp_acsl/bitwise_idemp.i, line 11):
+Assume {
+ Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(x).
+ (* Goal *)
+ When: if (x = 0) then (c = b) else (c = a).
+}
+Prove: land(a, land(b, c)) = land(a, b).
+
+------------------------------------------------------------
+
+Goal Check 'B' (file tests/wp_acsl/bitwise_idemp.i, line 12):
+Assume {
+ Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(x).
+ (* Goal *)
+ When: if (x = 0) then (c = b) else (c = a).
+}
+Prove: land(a, land(b, c)) = land(a, b).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function lor
+------------------------------------------------------------
+
+Goal Check 'A' (file tests/wp_acsl/bitwise_idemp.i, line 26):
+Assume {
+ Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(x).
+ (* Goal *)
+ When: if (x = 0) then (c = b) else (c = a).
+}
+Prove: lor(a, lor(b, c)) = lor(a, b).
+
+------------------------------------------------------------
+
+Goal Check 'B' (file tests/wp_acsl/bitwise_idemp.i, line 27):
+Assume {
+ Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(x).
+ (* Goal *)
+ When: if (x = 0) then (c = b) else (c = a).
+}
+Prove: lor(a, lor(b, c)) = lor(a, b).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function lxor
+------------------------------------------------------------
+
+Goal Check 'A' (file tests/wp_acsl/bitwise_idemp.i, line 40):
+Assume {
+ Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(e) /\
+ is_sint32(x).
+ (* Goal *)
+ When: if (x = 0) then ((c = b) /\ (e = a)) else ((c = a) /\ (e = b)).
+}
+Prove: lxor(a, lxor(b, c)) = e.
+
+------------------------------------------------------------
+
+Goal Check 'B' (file tests/wp_acsl/bitwise_idemp.i, line 41):
+Assume {
+ Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(e) /\
+ is_sint32(x).
+ (* Goal *)
+ When: if (x = 0) then ((c = b) /\ (e = a)) else ((c = a) /\ (e = b)).
+}
+Prove: lxor(a, lxor(b, c)) = e.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise_idemp.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise_idemp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f06b148b1571530b0853c53a0dd3c46f79ab88ab
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise_idemp.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/bitwise_idemp.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Alt-Ergo] Goal typed_land_check_A : Unsuccess
+[wp] [Alt-Ergo] Goal typed_land_check_B : Unsuccess
+[wp] [Alt-Ergo] Goal typed_lor_check_A : Unsuccess
+[wp] [Alt-Ergo] Goal typed_lor_check_B : Unsuccess
+[wp] [Alt-Ergo] Goal typed_lxor_check_A : Unsuccess
+[wp] [Alt-Ergo] Goal typed_lxor_check_B : Unsuccess
+[wp] Proved goals: 0 / 6
+ Alt-Ergo: 0 (unsuccess: 6)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ land - - 2 0.0%
+ lor - - 2 0.0%
+ lxor - - 2 0.0%
+------------------------------------------------------------