Add special case for &0 in the interval domain

goblint · Sep 11, 2023 · e40255b · e40255b
1 parent 4d18300
commit e40255b
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
@@ -835,7 +835,8 @@ struct
     | _ ->
       match to_int i1, to_int i2 with
       | Some x, Some y -> (try of_int ik (Ints_t.bitand x y) |> fst with Division_by_zero -> top_of ik)
-      | _, Some y  when Ints_t.equal y Ints_t.one -> of_interval ik (Ints_t.zero, Ints_t.one) |> fst
+      | _, Some y when Ints_t.equal y Ints_t.zero -> of_int ik Ints_t.zero |> fst
+      | _, Some y when Ints_t.equal y Ints_t.one -> of_interval ik (Ints_t.zero, Ints_t.one) |> fst
       | _ -> top_of ik
 
   let bitor  = bit (fun _ik -> Ints_t.bitor)