Suppress overflow warnings from IntDomTuple.of_const

These should currently never warn anyway, but suppressing them will allow avoiding unnecessary successful checks.

Author: sim642

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

@@ -119,7 +119,7 @@ module IntDomTupleImpl = struct
   let bot_of = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.bot_of }
   let of_bool ik = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.of_bool ik }
   let of_excl_list ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_excl_list ik}
-  let of_int ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_int ik }
+  let of_int ?(suppress_ovwarn=false) ik = create2_ovc ~suppress_ovwarn ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_int ik }
   let starting ?(suppress_ovwarn=false) ik = create2_ovc ~suppress_ovwarn ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.starting ik }
   let ending ?(suppress_ovwarn=false) ik = create2_ovc ~suppress_ovwarn ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.ending ik }
   let of_interval ?(suppress_ovwarn=false) ik = create2_ovc ~suppress_ovwarn ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_interval ik }
@@ -558,4 +558,4 @@ struct
   let no_bitfield (x: I.t) = {x with v = IntDomTupleImpl.no_bitfield x.v}
 end
 
-let of_const (i, ik, str) = IntDomTuple.of_int ik i
+let of_const (i, ik, str) = IntDomTuple.of_int ~suppress_ovwarn:true ik i

src/cdomain/value/cdomains/intDomain0.ml

@@ -166,7 +166,7 @@ struct
   let tag x = I.tag x.v
   let arbitrary ik = failwith @@ "Arbitrary not implement for " ^ (name ()) ^ "."
   let to_int x = I.to_int x.v
-  let of_int ikind x = { v = I.of_int ikind x; ikind}
+  let of_int ?(suppress_ovwarn=false) ikind x = { v = I.of_int ~suppress_ovwarn ikind x; ikind}
   let equal_to i x = I.equal_to i x.v
   let to_bool x = I.to_bool x.v
   let of_bool ikind b = { v = I.of_bool ikind b; ikind}
@@ -480,7 +480,7 @@ module SOverflowUnlifter (D : SOverflow) : S2 with type int_t = D.int_t and type
 
   let cast_to ?suppress_ovwarn ?torg ?no_ov ik x = fst @@ D.cast_to ?torg ?no_ov ik x
 
-  let of_int ik x = fst @@ D.of_int ik x
+  let of_int ?suppress_ovwarn ik x = fst @@ D.of_int ik x
 
   let of_interval ?suppress_ovwarn ik x = fst @@ D.of_interval ik x
 

src/cdomain/value/cdomains/intDomain_intf.ml

@@ -279,6 +279,7 @@ module type S2 =
 sig
   include S
 
+  val of_int: ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val starting : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val ending : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t
@@ -321,7 +322,7 @@ sig
   include Lattice.Top with type t := t
   include Arith with type t:=t
 
-  val of_int: Cil.ikind -> int_t -> t
+  val of_int: ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   (** Transform an integer literal to your internal domain representation with the specified ikind. *)
 
   val of_bool: Cil.ikind -> bool -> t

src/domains/intDomainProperties.ml

@@ -29,6 +29,7 @@ module MakeS2 (I: S): S2 =
 struct
   include I
 
+  let of_int ?suppress_ovwarn ik x = of_int ik x
   let starting ?suppress_ovwarn ik x = starting ik x
   let ending ?suppress_ovwarn ik x = ending ik x
   let of_interval ?suppress_ovwarn ik x = of_interval ik x