From e40255bdaca9bebe56ccde7f77ded60c25af9023 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 11 Sep 2023 12:52:13 +0200 Subject: [PATCH] Add special case for &0 in the interval domain --- src/cdomains/intDomain.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml index 312f5d7540..f1ed546e95 100644 --- 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)