Generalize positive def_exc ranges to not include 0

Author: sim642

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

@@ -110,10 +110,11 @@ struct
     | `Bot -> None
 
   let in_range r i =
-    if Z.compare i Z.zero < 0 then
+    (* if Z.compare i Z.zero < 0 then *)
       let lowerb = Exclusion.min_of_range r in
       Z.compare lowerb i <= 0
-    else
+      &&
+    (* else *)
       let upperb = Exclusion.max_of_range r in
       Z.compare i upperb <= 0
 
@@ -269,6 +270,9 @@ struct
      * just DeMorgans Law *)
     | `Excluded (x,r1), `Excluded (y,r2) ->
       let r' = R.meet r1 r2 in
+      if R.is_bot r' then
+        `Bot
+      else
       let s' = S.union x y |> S.filter (in_range r') in
       `Excluded (s', r')
 

src/cdomain/value/cdomains/intDomain0.ml

@@ -471,6 +471,10 @@ module Size = struct (* size in bits as int, range as int64 *)
     in
     if sign x = `Signed then
       size (min_for x)
+    else if Z.compare x Z.zero > 0 then (
+      let n = Int64.of_int (Z.numbits x) in
+      (Int64.pred n, n)
+    )
     else
       let a, b = size (min_for x) in
       if b <= 64L then
@@ -487,7 +491,7 @@ module Size = struct (* size in bits as int, range as int64 *)
   let max_from_bit_range pos_bits = Z.(pred @@ shift_left Z.one (to_int (Z.of_int64 pos_bits)))
 
   (* From the number of bits used to represent a non-positive value, determines the minimal representable value *)
-  let min_from_bit_range neg_bits = Z.(if neg_bits = 0L then Z.zero else neg @@ shift_left Z.one (to_int (neg (Z.of_int64 neg_bits))))
+  let min_from_bit_range neg_bits = Z.(if neg_bits = 0L then Z.zero else if neg_bits < 0L then neg @@ shift_left Z.one (to_int (neg (Z.of_int64 neg_bits))) else max_from_bit_range neg_bits)
 
 end