Assert valid state in bitfield domain witness invariant

Author: sim642

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

@@ -625,41 +625,38 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
   (* Invariant *)
 
   let invariant_ikind e ik (z, o) =
-    if BArith.is_invalid (z, o) then
-      Invariant.none (* TODO: should this ever even happen? *)
-    else (
-      let open GoblintCil.Cil in
-      let ik_type = TInt (ik, []) in
-      let i1 =
-        let def0 = z &: (!: o) in
-        if def0 =: BArith.zero_mask then
-          Invariant.none
-        else (
-          let def0 = Ints_t.to_bigint def0 in
-          if fitsInInt ik def0 then ( (* At least for _Bool and unsigned types, kintegerCilint can give an incorrect mask if doesn't fit. See https://github.com/goblint/analyzer/pull/1897/changes#r2610251390. *)
-            let def0 = kintegerCilint ik def0 in
-            Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def0, ik_type)), kintegerCilint ik Z.zero, intType))
-          )
-          else
-            Invariant.none
+    assert (not (BArith.is_invalid (z, o)));
+    let open GoblintCil.Cil in
+    let ik_type = TInt (ik, []) in
+    let i1 =
+      let def0 = z &: (!: o) in
+      if def0 =: BArith.zero_mask then
+        Invariant.none
+      else (
+        let def0 = Ints_t.to_bigint def0 in
+        if fitsInInt ik def0 then ( (* At least for _Bool and unsigned types, kintegerCilint can give an incorrect mask if doesn't fit. See https://github.com/goblint/analyzer/pull/1897/changes#r2610251390. *)
+          let def0 = kintegerCilint ik def0 in
+          Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def0, ik_type)), kintegerCilint ik Z.zero, intType))
         )
-      in
-      let i2 =
-        let def1 = o &: (!: z) in
-        if def1 =: BArith.zero_mask then
+        else
           Invariant.none
-        else (
-          let def1 = Ints_t.to_bigint def1 in
-          if fitsInInt ik def1 then ( (* At least for _Bool and unsigned types, kintegerCilint can give an incorrect mask if doesn't fit. See https://github.com/goblint/analyzer/pull/1897/changes#r2610251390. *)
-            let def1 = kintegerCilint ik def1 in
-            Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def1, ik_type)), def1, intType))
-          )
-          else
-            Invariant.none
+      )
+    in
+    let i2 =
+      let def1 = o &: (!: z) in
+      if def1 =: BArith.zero_mask then
+        Invariant.none
+      else (
+        let def1 = Ints_t.to_bigint def1 in
+        if fitsInInt ik def1 then ( (* At least for _Bool and unsigned types, kintegerCilint can give an incorrect mask if doesn't fit. See https://github.com/goblint/analyzer/pull/1897/changes#r2610251390. *)
+          let def1 = kintegerCilint ik def1 in
+          Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def1, ik_type)), def1, intType))
         )
-      in
-      Invariant.(i1 && i2)
-    )
+        else
+          Invariant.none
+      )
+    in
+    Invariant.(i1 && i2)
 
   let starting ik n =
     let (min_ik, max_ik) = Size.range ik in