Document def_exc and enums exclusion bit range assumption

Author: sim642

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

@@ -73,7 +73,7 @@ struct
 
 
   type t = [
-    | `Excluded of S.t * R.t
+    | `Excluded of S.t * R.t (** Bit range always includes 0. *)
     | `Definite of Z.t
     | `Bot
   ] [@@deriving eq, ord, hash]

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

@@ -11,7 +11,10 @@ module Enums : S with type int_t = Z.t = struct
   let range_ikind = Cil.IInt
   let size t = R.of_interval range_ikind (let a,b = Size.bits_i64 t in Int64.neg a,b)
 
-  type t = Inc of BISet.t | Exc of BISet.t * R.t [@@deriving eq, ord, hash] (* inclusion/exclusion set *)
+  type t =
+    | Inc of BISet.t (* Inclusion set. *)
+    | Exc of BISet.t * R.t (** Exclusion set. Bit range always includes 0. *)
+  [@@deriving eq, ord, hash]
 
   type int_t = Z.t
   let name () = "enums"

src/cdomain/value/cdomains/intDomain0.ml

@@ -464,6 +464,7 @@ module Size = struct (* size in bits as int, range as int64 *)
       if M.tracing then M.tracel "cast" "Cast %a to range [%a, %a] (%a) = %a (%s in int64)" GobZ.pretty x GobZ.pretty a GobZ.pretty b GobZ.pretty c GobZ.pretty y (if is_int64_big_int y then "fits" else "does not fit");
       y
 
+  (** @return Bit range always includes 0. *)
   let min_range_sign_agnostic x =
     let size ik =
       let a,b = bits_i64 ik in