diff --git a/src/cdomain/value/cdomains/int/bitfieldDomain.ml b/src/cdomain/value/cdomains/int/bitfieldDomain.ml index 5d504ec5e7..421ff4da89 100644 --- a/src/cdomain/value/cdomains/int/bitfieldDomain.ml +++ b/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 *) diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml index 178481089c..aef6b202d9 100644 --- a/src/cdomain/value/cdomains/int/congruenceDomain.ml +++ b/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) diff --git a/src/cdomain/value/cdomains/int/defExcDomain.ml b/src/cdomain/value/cdomains/int/defExcDomain.ml index 2b65051fe1..ab3ed821f0 100644 --- a/src/cdomain/value/cdomains/int/defExcDomain.ml +++ b/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! *) diff --git a/src/cdomain/value/cdomains/int/enumsDomain.ml b/src/cdomain/value/cdomains/int/enumsDomain.ml index 6768677bee..ce660d435a 100644 --- a/src/cdomain/value/cdomains/int/enumsDomain.ml +++ b/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 diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index e2dd683276..3d634ac6eb 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/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 } diff --git a/src/cdomain/value/cdomains/int/intervalDomain.ml b/src/cdomain/value/cdomains/int/intervalDomain.ml index ba8ca69f47..d5aa715e57 100644 --- a/src/cdomain/value/cdomains/int/intervalDomain.ml +++ b/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 = diff --git a/src/cdomain/value/cdomains/int/intervalSetDomain.ml b/src/cdomain/value/cdomains/int/intervalSetDomain.ml index 83c0e702fa..77642f384a 100644 --- a/src/cdomain/value/cdomains/int/intervalSetDomain.ml +++ b/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 diff --git a/src/cdomain/value/cdomains/intDomain0.ml b/src/cdomain/value/cdomains/intDomain0.ml index 9f9c588d28..ed7239cc08 100644 --- a/src/cdomain/value/cdomains/intDomain0.ml +++ b/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 diff --git a/src/cdomain/value/cdomains/intDomain_intf.ml b/src/cdomain/value/cdomains/intDomain_intf.ml index d3bd9b27d5..ae0c373556 100644 --- a/src/cdomain/value/cdomains/intDomain_intf.ml +++ b/src/cdomain/value/cdomains/intDomain_intf.ml @@ -248,8 +248,8 @@ sig val meet: Cil.ikind -> t -> t -> t val narrow: Cil.ikind -> t -> t -> t val widen: Cil.ikind -> t -> t -> t - val starting : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t - val ending : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t + val starting : Cil.ikind -> int_t -> t + val ending : Cil.ikind -> int_t -> t val of_int: Cil.ikind -> int_t -> t (** Transform an integer literal to your internal domain representation. *) @@ -257,7 +257,7 @@ sig (** Transform a known boolean value to the default internal representation. It * should follow C: [of_bool true = of_int 1] and [of_bool false = of_int 0]. *) - val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t + val of_interval: Cil.ikind -> int_t * int_t -> t val of_congruence: Cil.ikind -> int_t * int_t -> t val of_bitfield: Cil.ikind -> int_t * int_t -> t val to_bitfield: Cil.ikind -> t -> int_t * int_t @@ -275,6 +275,15 @@ sig end (** Interface of IntDomain implementations taking an ikind for arithmetic operations *) +module type S2 = +sig + include S + + 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 +end + module type SOverflow = sig @@ -290,14 +299,14 @@ sig val neg : ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info - val cast_to : ?suppress_ovwarn:bool -> ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info + val cast_to : ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info val of_int : Cil.ikind -> int_t -> t * overflow_info - val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t * overflow_info + val of_interval: Cil.ikind -> int_t * int_t -> t * overflow_info - val starting : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t * overflow_info - val ending : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t * overflow_info + val starting : Cil.ikind -> int_t -> t * overflow_info + val ending : Cil.ikind -> int_t -> t * overflow_info val shift_left : Cil.ikind -> t -> t -> t * overflow_info @@ -358,14 +367,15 @@ sig module type B = B module type IkindUnawareS = IkindUnawareS module type S = S + module type S2 = S2 module type SOverflow = SOverflow - module SOverflowUnlifter (D : SOverflow) : S with type int_t = D.int_t and type t = D.t + module SOverflowUnlifter (D : SOverflow) : S2 with type int_t = D.int_t and type t = D.t module type Y = Y module type Z = Z - module IntDomLifter (I: S): Y with type int_t = I.int_t + module IntDomLifter (I: S2): Y with type int_t = I.int_t module type Ikind = Ikind diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml index 155be6f90a..392f56b0c0 100644 --- a/src/domains/intDomainProperties.ml +++ b/src/domains/intDomainProperties.ml @@ -23,9 +23,19 @@ sig end module type S = IntDomain.S with type int_t = Z.t +module type S2 = IntDomain.S2 with type int_t = Z.t + +module MakeS2 (I: S): S2 = +struct + include I + + 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 +end (* TODO: deduplicate with IntDomain, extension of IntDomWithDefaultIkind, inverse of OldDomainFacade? *) -module WithIkind (I: S) (Ik: IntDomain.Ikind): OldSWithIkind = +module WithIkind (I: S2) (Ik: IntDomain.Ikind): OldSWithIkind = struct include I module Ikind = Ik diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index 1239df1f1d..af52b14abd 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -115,11 +115,11 @@ end module Ikind = struct let ikind () = Cil.ILong end module A = IntTest (IntDomain.Integers (IntOps.BigIntOps)) module B = IntTest (IntDomain.Flat (IntDomain.Integers (IntOps.BigIntOps))) -module C = IntTest (IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind)) +module C = IntTest (IntDomainProperties.WithIkind (IntDomainProperties.MakeS2 (IntDomain.DefExc)) (Ikind)) module D = struct module T = struct - include IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind) + include IntDomainProperties.WithIkind (IntDomainProperties.MakeS2 (IntDomain.DefExc)) (Ikind) let of_excl_list xs = of_excl_list Cil.ILong xs end diff --git a/tests/unit/cdomains/lvalTest.ml b/tests/unit/cdomains/lvalTest.ml index adaa7cfde1..97846f9f50 100644 --- a/tests/unit/cdomains/lvalTest.ml +++ b/tests/unit/cdomains/lvalTest.ml @@ -2,7 +2,7 @@ open Goblint_lib open OUnit2 open GoblintCil -module ID = IntDomain.IntDomWithDefaultIkind (IntDomain.IntDomLifter (IntDomain.DefExc)) (IntDomain.PtrDiffIkind) +module ID = IntDomain.IntDomWithDefaultIkind (IntDomain.IntDomLifter (IntDomainProperties.MakeS2 (IntDomain.DefExc))) (IntDomain.PtrDiffIkind) module Offs = Offset.MakeLattice (ID) module LV = AddressDomain.AddressLattice (Mval.MakeLattice (Offs)) diff --git a/tests/unit/maindomaintest.ml b/tests/unit/maindomaintest.ml index b6af01ff6f..aab5978c49 100644 --- a/tests/unit/maindomaintest.ml +++ b/tests/unit/maindomaintest.ml @@ -41,10 +41,10 @@ let domains: (module Lattice.S) list = [ let nonAssocDomains: (module Lattice.S) list = [] -let intDomains: (module IntDomainProperties.S) list = [ +let intDomains: (module IntDomainProperties.S2) list = [ (module IntDomain.SOverflowUnlifter(IntDomain.Interval)); - (module IntDomain.Enums); - (module IntDomain.Congruence); + (module IntDomainProperties.MakeS2 (IntDomain.Enums)); + (module IntDomainProperties.MakeS2 (IntDomain.Congruence)); (module IntDomain.SOverflowUnlifter(IntDomain.IntervalSet)); (module IntDomain.SOverflowUnlifter(IntDomain.Bitfield)); (* (module IntDomain.Flattened); *) @@ -53,8 +53,8 @@ let intDomains: (module IntDomainProperties.S) list = [ (* (module IntDomain.IntDomTuple); *) ] -let nonAssocIntDomains: (module IntDomainProperties.S) list = [ - (module IntDomain.DefExc); +let nonAssocIntDomains: (module IntDomainProperties.S2) list = [ + (module IntDomainProperties.MakeS2 (IntDomain.DefExc)); ] (* TODO: make arbitrary ikind part of domain test for better efficiency *) @@ -91,7 +91,7 @@ let nonAssocTestsuite = let old_intdomains intDomains = BatList.cartesian_product intDomains ikinds |> List.map (fun (d, ik) -> - let module D = (val d: IntDomainProperties.S) in + let module D = (val d: IntDomainProperties.S2) in let module Ikind = struct let ikind () = ik end in (module IntDomainProperties.WithIkind (D) (Ikind): IntDomainProperties.OldSWithIkind) ) diff --git a/tests/unit/solver/solverTest.ml b/tests/unit/solver/solverTest.ml index a33ab061f7..1bc04354d5 100644 --- a/tests/unit/solver/solverTest.ml +++ b/tests/unit/solver/solverTest.ml @@ -23,7 +23,7 @@ end (* domain is (reversed) integers *) module Ikind = struct let ikind () = Cil.ILong end -module Int = IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind) +module Int = IntDomainProperties.WithIkind (IntDomainProperties.MakeS2 (IntDomain.DefExc)) (Ikind) module IntR = Lattice.Reverse(Int) module ConstrSys = struct