Merge pull request #1815 from goblint/suppress_ovwarn

Remove some unnecessary `suppress_ovwarn` arguments

Author: sim642

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

@@ -253,7 +253,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
       let newo = o &: (Ints_t.of_bigint max_ik) in
       (newz,newo)
 
-  let norm ?(suppress_ovwarn=false) ?(ov=false) ik (z,o) =
+  let norm ?(ov=false) ik (z,o) =
     if BArith.is_invalid (z,o) then
       bot ()
     else
@@ -263,7 +263,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
       else
         top_of ik
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) ik (z,o) =
+  let cast_to ?torg ?(no_ov=false) ik (z,o) =
     let (min_ik, max_ik) = Size.range ik in
     let (underflow, overflow) = match torg with
       | None -> (false, false) (* ik does not change *)
@@ -278,10 +278,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
         let overflow = (((!:(Ints_t.of_bigint max_ik)) &: o) <>: Ints_t.zero) && isPos in
         (underflow, overflow)
     in
-    let overflow_info = if suppress_ovwarn then {underflow=false; overflow=false} else {underflow=underflow; overflow=overflow} in
-    (norm ~suppress_ovwarn:(suppress_ovwarn) ~ov:(underflow || overflow) ik (z,o), overflow_info)
+    let overflow_info = {underflow; overflow} in
+    (norm ~ov:(underflow || overflow) ik (z,o), overflow_info)
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) ik (z,o) =
+  let cast_to ?torg ?(no_ov=false) ik (z,o) =
     if ik = GoblintCil.IBool then (
       let may_zero =
         if Ints_t.equal z BArith.one_mask then (* zero bit may be in every position (one_mask) *)
@@ -298,7 +298,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
       (BArith.join may_zero may_one, {underflow=false; overflow=false})
     )
     else
-      cast_to ~suppress_ovwarn ?torg ~no_ov ik (z,o)
+      cast_to ?torg ~no_ov ik (z,o)
 
   let join ik b1 b2 = norm ik @@ (BArith.join b1 b2)
 
@@ -335,7 +335,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
 
   type bit_status = Zero | One | Top
 
-  let of_interval ?(suppress_ovwarn=false) ik (x,y) =
+  let of_interval ik (x,y) =
     let (min_ik, max_ik) = Size.range ik in
     let startv = Ints_t.max x (Ints_t.of_bigint min_ik) in
     let endv= Ints_t.min y (Ints_t.of_bigint max_ik) in
@@ -638,13 +638,13 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
       let exp1 = Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def1, TInt(ik,[]))), def1, intType)) in
       Invariant.meet exp0 exp1
 
-  let starting ?(suppress_ovwarn=false) ik n =
+  let starting ik n =
     let (min_ik, max_ik) = Size.range ik in
-    of_interval ~suppress_ovwarn ik (n, Ints_t.of_bigint max_ik)
+    of_interval ik (n, Ints_t.of_bigint max_ik)
 
-  let ending ?(suppress_ovwarn=false) ik n =
+  let ending ik n =
     let (min_ik, max_ik) = Size.range ik in
-    of_interval ~suppress_ovwarn ik (Ints_t.of_bigint min_ik, n)
+    of_interval ik (Ints_t.of_bigint min_ik, n)
 
   (* Refinements *)
 

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

@@ -133,9 +133,10 @@ struct
     | x when equal zero x -> Some false
     | x -> if leq zero x then None else Some true
 
-  let starting ?(suppress_ovwarn=false) ik n = top()
+  let starting ik n = top()
 
   let ending = starting
+  let of_interval ik x = of_interval ik x (* cast away optional suppress_ovwarn argument *)
 
   let of_congruence ik (c,m) = normalize ik @@ Some(c,m)
 

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

@@ -298,12 +298,12 @@ struct
     | _ -> None
   let top_bool = `Excluded (S.empty (), R.of_interval range_ikind (0L, 1L))
 
-  let of_interval ?(suppress_ovwarn=false) ik (x,y) =
+  let of_interval ik (x,y) =
     if Z.compare x y = 0 then
       of_int ik x
     else
       let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in
-      let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval ~suppress_ovwarn range_ikind b) in
+      let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in
       let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else  S.empty () in
       norm ik @@ (`Excluded (ex, r))
 
@@ -318,13 +318,13 @@ struct
       let ik_mask = snd (Size.range ik) in
       (one_mask, ik_mask)
 
-  let starting ?(suppress_ovwarn=false) ikind x =
+  let starting ikind x =
     let _,u_ik = Size.range ikind in
-    of_interval ~suppress_ovwarn ikind (x, u_ik)
+    of_interval ikind (x, u_ik)
 
-  let ending ?(suppress_ovwarn=false) ikind x =
+  let ending ikind x =
     let l_ik,_ = Size.range ikind in
-    of_interval ~suppress_ovwarn ikind (l_ik, x)
+    of_interval ikind (l_ik, x)
 
   let of_excl_list t l =
     let r = size t in (* elements in l are excluded from the full range of t! *)

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

@@ -119,12 +119,12 @@ module Enums : S with type int_t = Z.t = struct
 
   let of_int ikind x = cast_to ikind (Inc (BISet.singleton x))
 
-  let of_interval ?(suppress_ovwarn=false) ik (x, y) =
+  let of_interval ik (x, y) =
     if Z.compare x y = 0 then
       of_int ik x
     else
       let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in
-      let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval ~suppress_ovwarn range_ikind b) in
+      let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in
       let ex = if Z.gt x Z.zero || Z.lt y Z.zero then BISet.singleton Z.zero else BISet.empty () in
       norm ik @@ (Exc (ex, r))
 
@@ -380,13 +380,13 @@ module Enums : S with type int_t = Z.t = struct
     | _ when Cil.isSigned ik -> (one_mask, one_mask)
     | _ -> (one_mask, ik_mask)
 
-  let starting ?(suppress_ovwarn=false) ikind x =
+  let starting ikind x =
     let _,u_ik = Size.range ikind in
-    of_interval ~suppress_ovwarn ikind (x, u_ik)
+    of_interval ikind (x, u_ik)
 
-  let ending ?(suppress_ovwarn=false) ikind x =
+  let ending ikind x =
     let l_ik,_ = Size.range ikind in
-    of_interval ~suppress_ovwarn ikind (l_ik, x)
+    of_interval ikind (l_ik, x)
 
   let c_lognot ik x =
     if is_bot x

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

@@ -76,17 +76,17 @@ module IntDomTupleImpl = struct
     );
     no_ov
 
-  let create2_ovc ik r x ((p1, p2, p3, p4, p5, p6): int_precision) =
+  let create2_ovc ?(suppress_ovwarn = false) ik r x ((p1, p2, p3, p4, p5, p6): int_precision) =
     let f b g = if b then Some (g x) else None in
     let map x = Option.map fst x in
     let intv =  f p2 @@ r.fi2_ovc (module I2) in
     let intv_set = f p5 @@ r.fi2_ovc (module I5) in
     let bf = f p6 @@ r.fi2_ovc (module I6) in
-    ignore (check_ov ~cast:false ik intv intv_set bf);
+    ignore (check_ov ~suppress_ovwarn ~cast:false ik intv intv_set bf);
     map @@ f p1 @@ r.fi2_ovc (module I1), map @@ f p2 @@ r.fi2_ovc (module I2), map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map @@ f p5 @@ r.fi2_ovc (module I5) , map @@ f p6 @@ r.fi2_ovc (module I6)
 
-  let create2_ovc ik r x = (* use where values are introduced *)
-    create2_ovc ik r x (int_precision_from_node_or_config ())
+  let create2_ovc ?(suppress_ovwarn = false) ik r x = (* use where values are introduced *)
+    create2_ovc ~suppress_ovwarn ik r x (int_precision_from_node_or_config ())
 
 
   let opt_map2 f ?no_ov =
@@ -120,9 +120,9 @@ module IntDomTupleImpl = struct
   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 starting ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.starting ~suppress_ovwarn ik }
-  let ending ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.ending ~suppress_ovwarn ik }
-  let of_interval ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_interval ~suppress_ovwarn 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 }
   let of_congruence ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_congruence ik }
   let of_bitfield ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_bitfield ik }
 

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

@@ -32,14 +32,14 @@ struct
     | Some (a, b) ->
       if a = b && b = i then `Eq else if Ints_t.compare a i <= 0 && Ints_t.compare i b <=0 then `Top else `Neq
 
-  let norm ?(suppress_ovwarn=false) ?(cast=false) ik : (t -> t * overflow_info) = function None -> (None, {underflow=false; overflow=false}) | Some (x,y) ->
+  let norm ?(cast=false) ik : (t -> t * overflow_info) = function None -> (None, {underflow=false; overflow=false}) | Some (x,y) ->
     if Ints_t.compare x y > 0 then
       (None,{underflow=false; overflow=false})
     else (
       let (min_ik, max_ik) = range ik in
       let underflow = Ints_t.compare min_ik x > 0 in
       let overflow = Ints_t.compare max_ik y < 0 in
-      let ov_info = { underflow = underflow && not suppress_ovwarn; overflow = overflow && not suppress_ovwarn } in
+      let ov_info = { underflow; overflow } in
       let v =
         if underflow || overflow then
           if should_wrap ik then (* could add [|| cast], but that's GCC implementation-defined behavior: https://gcc.gnu.org/onlinedocs/gcc/Integers-implementation.html#Integers-implementation *)
@@ -88,7 +88,7 @@ struct
 
   (* TODO: change to_int signature so it returns a big_int *)
   let to_int x = Option.bind x (IArith.to_int)
-  let of_interval ?(suppress_ovwarn=false) ik (x,y) = norm ~suppress_ovwarn ik @@ Some (x,y)
+  let of_interval ik (x,y) = norm ik @@ Some (x,y)
 
   let of_bitfield ik x =
     let min ik (z,o) =
@@ -129,17 +129,17 @@ struct
     | Some (l, u) when Ints_t.compare l Ints_t.zero = 0 && Ints_t.compare u Ints_t.zero = 0 -> Some false
     | x -> if leq zero x then None else Some true
 
-  let starting ?(suppress_ovwarn=false) ik n =
-    norm ~suppress_ovwarn ik @@ Some (n, snd (range ik))
+  let starting ik n =
+    norm ik @@ Some (n, snd (range ik))
 
-  let ending ?(suppress_ovwarn=false) ik n =
-    norm ~suppress_ovwarn ik @@ Some (fst (range ik), n)
+  let ending ik n =
+    norm ik @@ Some (fst (range ik), n)
 
   (* TODO: change signature of maximal, minimal to return big_int*)
   let maximal = function None -> None | Some (x,y) -> Some y
   let minimal = function None -> None | Some (x,y) -> Some x
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *)
+  let cast_to ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *)
 
   let widen ik x y =
     match x, y with
@@ -524,7 +524,7 @@ struct
       let l' = if Ints_t.equal l min_ik then l else shrink Ints_t.add l in
       let u' = if Ints_t.equal u max_ik then u else shrink Ints_t.sub u in
       let intv' = norm ik @@ Some (l', u') |> fst in
-      let range = norm ~suppress_ovwarn:true ik (Some (Ints_t.of_bigint (Size.min_from_bit_range rl), Ints_t.of_bigint (Size.max_from_bit_range rh))) |> fst in
+      let range = norm ik (Some (Ints_t.of_bigint (Size.min_from_bit_range rl), Ints_t.of_bigint (Size.max_from_bit_range rh))) |> fst in
       meet ik intv' range
 
   let refine_with_incl_list ik (intv: t) (incl : (int_t list) option) : t =

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

@@ -141,7 +141,7 @@ struct
     | ys when List.for_all ((=) `Neq) ys -> `Neq
     | _ -> `Top
 
-  let norm_interval ?(suppress_ovwarn=false) ?(cast=false) ik (x,y) : t*overflow_info =
+  let norm_interval ?(cast=false) ik (x,y) : t*overflow_info =
     if x >. y then
       ([],{underflow=false; overflow=false})
     else
@@ -173,10 +173,10 @@ struct
         else
           [(x,y)]
       in
-      if suppress_ovwarn then (v, {underflow=false; overflow=false}) else (v, {underflow; overflow})
+      (v, {underflow; overflow})
 
-  let norm_intvs ?(suppress_ovwarn=false) ?(cast=false) (ik:ikind) (xs: t) : t*overflow_info =
-    let res = List.map (norm_interval ~suppress_ovwarn ~cast ik) xs in
+  let norm_intvs ?(cast=false) (ik:ikind) (xs: t) : t*overflow_info =
+    let res = List.map (norm_interval ~cast ik) xs in
     let intvs = List.concat_map fst res in
     let underflow = List.exists (fun (_,{underflow; _}) -> underflow) res in
     let overflow = List.exists (fun (_,{overflow; _}) -> overflow) res in
@@ -249,7 +249,7 @@ struct
 
   let of_bool _ = function true -> one | false -> zero
 
-  let of_interval ?(suppress_ovwarn=false) ik (x,y) =  norm_interval  ~suppress_ovwarn ~cast:false ik (x,y)
+  let of_interval ik (x,y) =  norm_interval ~cast:false ik (x,y)
 
   let of_bitfield ik x =
     match Interval.of_bitfield ik x with
@@ -484,7 +484,7 @@ struct
     in
     binop x y interval_rem
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov ik x = norm_intvs ~cast:true ik x
+  let cast_to ?torg ?no_ov ik x = norm_intvs ~cast:true ik x
 
   (*
       narrows down the extremeties of xs if they are equal to boundary values of the ikind with (possibly) narrower values from ys
@@ -572,9 +572,9 @@ struct
     in
     interval_sets_to_partitions ik xs ys |> merge_list ik |> widen_left |> widen_right |> List.map snd
 
-  let starting ?(suppress_ovwarn=false) ik n = norm_interval ik ~suppress_ovwarn (n, snd (range ik))
+  let starting ik n = norm_interval ik (n, snd (range ik))
 
-  let ending ?(suppress_ovwarn=false) ik n = norm_interval ik ~suppress_ovwarn (fst (range ik), n)
+  let ending ik n = norm_interval ik (fst (range ik), n)
 
   let invariant_ikind e ik xs =
     List.map (fun x -> Interval.invariant_ikind e ik (Some x)) xs |>
@@ -620,7 +620,7 @@ struct
   let excl_range_to_intervalset (ik: ikind) ((min, max): int_t * int_t) (excl: int_t): t =
     let intv1 = (min, excl -. Ints_t.one) in
     let intv2 = (excl +. Ints_t.one, max) in
-    norm_intvs ik ~suppress_ovwarn:true [intv1 ; intv2] |> fst
+    norm_intvs ik [intv1 ; intv2] |> fst
 
   let of_excl_list ik (excls: int_t list) =
     let excl_list = List.map (excl_range_to_intervalset ik (range ik)) excls in

src/cdomain/value/cdomains/intDomain0.ml

@@ -110,7 +110,7 @@ sig
 end
 
 
-module IntDomLifter (I : S) =
+module IntDomLifter (I : S2) =
 struct
   open Cil
   type int_t = I.int_t
@@ -477,7 +477,7 @@ struct
       ) (Invariant.top ()) ns
 end
 
-module SOverflowUnlifter (D : SOverflow) : S with type int_t = D.int_t and type t = D.t = struct
+module SOverflowUnlifter (D : SOverflow) : S2 with type int_t = D.int_t and type t = D.t = struct
   include D
 
   let add ?no_ov ik x y = fst @@ D.add ?no_ov ik x y
@@ -490,15 +490,15 @@ module SOverflowUnlifter (D : SOverflow) : S with type int_t = D.int_t and type
 
   let neg ?no_ov ik x = fst @@ D.neg ?no_ov ik x
 
-  let cast_to ?suppress_ovwarn ?torg ?no_ov ik x = fst @@ D.cast_to ?suppress_ovwarn ?torg ?no_ov ik x
+  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_interval ?suppress_ovwarn ik x = fst @@ D.of_interval ?suppress_ovwarn ik x
+  let of_interval ?suppress_ovwarn ik x = fst @@ D.of_interval ik x
 
-  let starting ?suppress_ovwarn ik x = fst @@ D.starting ?suppress_ovwarn ik x
+  let starting ?suppress_ovwarn ik x = fst @@ D.starting ik x
 
-  let ending ?suppress_ovwarn ik x = fst @@ D.ending ?suppress_ovwarn ik x
+  let ending ?suppress_ovwarn ik x = fst @@ D.ending ik x
 
   let shift_left ik x y = fst @@ D.shift_left ik x y
 
@@ -742,15 +742,15 @@ module SOverflowLifter (D : S) : SOverflow with type int_t = D.int_t and type t
 
   let neg ?no_ov ik x = lift @@ D.neg ?no_ov ik x
 
-  let cast_to ?suppress_ovwarn ?torg ?no_ov ik x = lift @@ D.cast_to ?suppress_ovwarn ?torg ?no_ov ik x
+  let cast_to ?torg ?no_ov ik x = lift @@ D.cast_to ?torg ?no_ov ik x
 
   let of_int ik x = lift @@ D.of_int ik x
 
-  let of_interval ?suppress_ovwarn ik x = lift @@ D.of_interval ?suppress_ovwarn ik x
+  let of_interval ik x = lift @@ D.of_interval ik x
 
-  let starting ?suppress_ovwarn ik x = lift @@ D.starting ?suppress_ovwarn ik x
+  let starting ik x = lift @@ D.starting ik x
 
-  let ending ?suppress_ovwarn ik x = lift @@ D.ending ?suppress_ovwarn ik x
+  let ending ik x = lift @@ D.ending ik x
 
   let shift_left ik x y = lift @@ D.shift_left ik x y