Fix bitfield _Bool casts

Author: sim642

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

@@ -281,6 +281,25 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
     let overflow_info = if suppress_ovwarn then {underflow=false; overflow=false} else {underflow=underflow; overflow=overflow} in
     (norm ~suppress_ovwarn:(suppress_ovwarn) ~ov:(underflow || overflow) ik (z,o), overflow_info)
 
+  let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) ik (z,o) =
+    if ik = GoblintCil.IBool then (
+      let may_zero =
+        if Ints_t.equal z BArith.one_mask then (* zero bit may be in every position (one_mask) *)
+          BArith.zero
+        else
+          bot () (* must be non-zero, so may not be zero *)
+      in
+      let may_one =
+        if Ints_t.equal o BArith.zero_mask then (* one bit may be in no position (zero_mask) *)
+          bot () (* must be zero, so may not be one *)
+        else
+          BArith.one
+      in
+      (BArith.join may_zero may_one, {underflow=false; overflow=false})
+    )
+    else
+      cast_to ~suppress_ovwarn ?torg ~no_ov ik (z,o)
+
   let join ik b1 b2 = norm ik @@ (BArith.join b1 b2)
 
   let meet ik x y = norm ik @@ (BArith.meet x y)

tests/regression/83-bitfield/14-bool.c

@@ -12,23 +12,23 @@ int main() {
 
   // assigning constant from other variable instead of integer constant, because integer constant swallows implicit cast to _Bool
   _Bool b1 = i1;
-  _Bool b123 = i123; // TODO NOWARN (overflow)
-  _Bool bm123 = im123; // TODO NOWARN (underflow)
-  _Bool b128 = i128; // TODO NOWARN (overflow)
-  _Bool bm128 = im128; // TODO NOWARN (underflow)
+  _Bool b123 = i123; // NOWARN (overflow)
+  _Bool bm123 = im123; // NOWARN (underflow)
+  _Bool b128 = i128; // NOWARN (overflow)
+  _Bool bm128 = im128; // NOWARN (underflow)
   _Bool bf = i0;
-  _Bool brand = irand; // TODO NOWARN (underflow, overflow)
+  _Bool brand = irand; // NOWARN (underflow, overflow)
 
   __goblint_check(b1);
   __goblint_check(b1 == 1);
   __goblint_check(b123);
   __goblint_check(b123 == 1);
   __goblint_check(bm123);
   __goblint_check(bm123 == 1);
-  __goblint_check(b128); // TODO
-  __goblint_check(b128 == 1); // TODO
-  __goblint_check(bm128); // TODO
-  __goblint_check(bm128 == 1); // TODO
+  __goblint_check(b128);
+  __goblint_check(b128 == 1);
+  __goblint_check(bm128);
+  __goblint_check(bm128 == 1);
   __goblint_check(!bf);
   __goblint_check(bf == 0);
   __goblint_check(brand); // UNKNOWN!