Simplify bitfield witness invariant for definite zeroes

Author: sim642

src/cdomain/value/cdomains/int/bitfieldDomain.ml

@@ -636,7 +636,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
           Invariant.none
         else (
           let def0 = kintegerCilint ik (Ints_t.to_bigint def0) in
-          Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, UnOp (BNot, e, ik_type), def0, ik_type)), def0, intType))
+          Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def0, ik_type)), kintegerCilint ik Z.zero, intType))
         )
       in
       let i2 =

tests/regression/56-witness/46-top-bool-invariant.t

@@ -178,7 +178,7 @@ bitfield only:
           line: 5
           column: 3
           function: main
-        value: (~ x & (_Bool)1) == (_Bool)1
+        value: (x & (_Bool)1) == (_Bool)0
         format: c_expression
     - invariant:
         type: location_invariant

tests/regression/83-bitfield/00-simple-demo.t

@@ -164,7 +164,7 @@
           line: 28
           column: 3
           function: main
-        value: (~ state & -11) == -11
+        value: (state & -11) == 0
         format: c_expression
     - invariant:
         type: location_invariant
@@ -200,7 +200,7 @@
           line: 29
           column: 1
           function: main
-        value: (~ state & -11) == -11
+        value: (state & -11) == 0
         format: c_expression
     - invariant:
         type: location_invariant

tests/regression/witness/int.t/run.t

@@ -31,7 +31,7 @@
           line: 12
           column: 5
           function: main
-        value: (51 <= i && i <= 99) && (~ i & (-0x7FFFFFFF-1)) == (-0x7FFFFFFF-1)
+        value: (51 <= i && i <= 99) && (i & (-0x7FFFFFFF-1)) == 0
         format: c_expression
     - invariant:
         type: location_invariant