diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index a796a6045df2e579cdd00f58e6e40d76d997cf0c..0b9c00f9c279ba44ebd35381f70c86b138036d94 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -590,6 +590,15 @@ let smp_shift zf = (* f(e1,0)~>e1, c2>0==>f(c1,c2)~>zf(c1,c2), c2>0==>f(0,c2)~>0
end
| _ -> raise Not_found
+let smp_lnot = function
+ | ([e] as args) -> begin match F.repr e with
+ | Logic.Fun( f , [e] ) when Fun.equal f f_lnot ->
+ (* ~~e ~> e *)
+ e
+ | _ -> smp1 Integer.lognot args
+ end
+ | _ -> raise Not_found
+
(* -------------------------------------------------------------------------- *)
(* --- Comparision with L-AND / L-OR / L-NOT --- *)
(* -------------------------------------------------------------------------- *)
@@ -647,11 +656,15 @@ let smp_eq_with_lxor a b = (* b1==(a2^e) <==> (b1^a2)==e *)
| e1::((_::_) as e22) -> e_eq e1 (e_fun f_lnot [e_fun f_lxor e22])
| _ -> raise Not_found)
-let smp_eq_with_lnot a b = (* b1==~e <==> ~b1==e *)
- let b1 = match_integer b in
+let smp_eq_with_lnot a b =
let e = match_ufun f_lnot a in
- let k1 = Integer.lognot b1 in
- e_eq (e_zint k1) e
+ try (* b1==~e <==> ~b1==e *)
+ let b1 = match_integer b in
+ let k1 = Integer.lognot b1 in
+ e_eq (e_zint k1) e
+ with Not_found ->(* ~b==~e <==> b==e *)
+ let b = match_ufun f_lnot b in
+ e_eq e b
(* -------------------------------------------------------------------------- *)
(* --- Comparision with LSL / LSR --- *)
@@ -807,8 +820,7 @@ let () =
no creation of [e_fun f_bit_stdlib args] *)
let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
- let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot
- (smp1 Integer.lognot) in
+ let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot smp_lnot in
let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
(smp2 f_lxor Integer.logxor) in
let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor
diff --git a/src/plugins/wp/tests/wp_acsl/bitwise.i b/src/plugins/wp/tests/wp_acsl/bitwise.i
index 79dab19ec7b88508eb91b7ed031059e5a90695e1..a77559d8fc218a0afcc8f465b092337fc99a6594 100644
--- a/src/plugins/wp/tests/wp_acsl/bitwise.i
+++ b/src/plugins/wp/tests/wp_acsl/bitwise.i
@@ -48,7 +48,7 @@ int bor(int a,int b, int c) { return a | b | c ; }
@ ensures \result == 0;
@ behavior bit3:
@ assumes a == ~b;
- @ ensures zbit: \result == -1;
+ @ ensures \result == -1;
*/
int bxor(int a,int b) { return a ^ b ; }
@@ -100,3 +100,14 @@ _Bool band_bool(_Bool a, _Bool b) { return (_Bool)(((int)a & (int)b) != 0); }
@ ensures \result == 0;
*/
_Bool bxor_bool(_Bool a, _Bool b) { return (_Bool)(((int)a ^ (int)b) != 0); }
+
+void lemma(unsigned a, unsigned b) {
+ //@ check zbit: a1: ~(a + ~a) == 0;
+ //@ check zbit: a2: ~(a | ~a) == 0;
+ //@ check zbit: a3: (a & ~a) == 0;
+ //@ check ~(a ^ ~a) == 0;
+ //@ check (a ^ a) == 0;
+ //@ check (~a --> a) == a;
+ //@ check (a --> ~a) == ~a;
+ //@ check (~a == ~b) ==> (a == b);
+}
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 320a3fd9ef45d2ece137443e12d54dc8fd2b4ecb..28ba63538071fd70596d7abb89270ce8eccab41b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
@@ -189,10 +189,8 @@ Prove: true.
Function bxor with behavior bit3
------------------------------------------------------------
-Goal Post-condition for 'bit3' 'zbit' in 'bxor':
-Let x = lnot(b).
-Assume { Type: is_sint32(b) /\ is_sint32(x) /\ is_sint32(lxor(b, x)). }
-Prove: lnot(x) = b.
+Goal Post-condition for 'bit3' (file tests/wp_acsl/bitwise.i, line 51) in 'bxor':
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -220,6 +218,52 @@ Assume {
}
Prove: b != a.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function lemma
+------------------------------------------------------------
+
+Goal Check 'zbit,a1' (file tests/wp_acsl/bitwise.i, line 105):
+Assume { Type: is_uint32(a). }
+Prove: (a + lnot(a)) = (-1).
+
+------------------------------------------------------------
+
+Goal Check 'zbit,a2' (file tests/wp_acsl/bitwise.i, line 106):
+Assume { Type: is_uint32(a). }
+Prove: lor(a, lnot(a)) = (-1).
+
+------------------------------------------------------------
+
+Goal Check 'zbit,a3' (file tests/wp_acsl/bitwise.i, line 107):
+Assume { Type: is_uint32(a). }
+Prove: land(a, lnot(a)) = 0.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/bitwise.i, line 108):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/bitwise.i, line 109):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/bitwise.i, line 110):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/bitwise.i, line 111):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/bitwise.i, line 112):
+Prove: true.
+
------------------------------------------------------------
------------------------------------------------------------
Function lshift
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 a91b7a0149b5b87b9fc08bf7b402236915adc151..80f6858702b19a9d7120dbb5674ac19d51efd96f 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 tests/wp_acsl/bitwise.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 29 goals scheduled
+[wp] 35 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
@@ -19,6 +19,7 @@
[wp] [Qed] Goal typed_bxor_ensures : Valid
[wp] [Qed] Goal typed_bxor_bit1_ensures : Valid
[wp] [Qed] Goal typed_bxor_bit2_ensures : Valid
+[wp] [Qed] Goal typed_bxor_bit3_ensures : Valid
[wp] [Qed] Goal typed_bnot_ensures : Valid
[wp] [Qed] Goal typed_lshift_ensures : Valid
[wp] [Qed] Goal typed_lshift_shift1_ensures_lsl1 : Valid
@@ -32,18 +33,24 @@
[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Valid
[wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Valid
-[wp] Proved goals: 29 / 29
- Qed: 25
+[wp] [Qed] Goal typed_lemma_check : Valid
+[wp] [Qed] Goal typed_lemma_check_2 : Valid
+[wp] [Qed] Goal typed_lemma_check_3 : Valid
+[wp] [Qed] Goal typed_lemma_check_4 : Valid
+[wp] [Qed] Goal typed_lemma_check_5 : Valid
+[wp] Proved goals: 35 / 35
+ Qed: 31
Alt-Ergo: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
band 8 - 8 100%
bor 5 - 5 100%
- bxor 3 - 3 100%
+ bxor 4 - 4 100%
bnot 1 - 1 100%
lshift 4 - 4 100%
rshift 2 - 2 100%
bor_bool - 2 2 100%
band_bool 1 1 2 100%
bxor_bool 1 1 2 100%
+ lemma 5 - 5 100%
------------------------------------------------------------