diff --git a/src/kernel_services/abstract_interp/lattice_bounds.mli b/src/kernel_services/abstract_interp/lattice_bounds.mli index 9b444d32611eef76632a75e2d37034436c38384a..faba7e98261e2cacfee8b359422ac232ce7a86cc 100644 --- a/src/kernel_services/abstract_interp/lattice_bounds.mli +++ b/src/kernel_services/abstract_interp/lattice_bounds.mli @@ -63,9 +63,6 @@ module Bottom : sig (* Iterators *) val iter : ('a -> unit) -> 'a t -> unit - (* Combination *) - val zip : 'a t -> 'b t -> ('a * 'b) t (* `Bottom if any is `Bottom *) - (** In a lattice where the elements are lists of non-bottom values, the empty list is the bottom case. *) @@ -113,9 +110,6 @@ module Top : sig (* Iterators *) val iter : ('a -> unit) -> 'a t -> unit - (** Combination *) - val zip : 'a t -> 'b t -> ('a * 'b) t (* `Top if any is `Top *) - (** Conversion *) val to_option : 'a t -> 'a option val of_option : 'a option -> 'a t diff --git a/src/plugins/eva/contexts/context_product.ml b/src/plugins/eva/contexts/context_product.ml index 4ca41b8fdc1ce92d1c2531b5afcd4dfade1ba9a6..072bb1824f816d48291b216c8a7b4c664bad1a05 100644 --- a/src/plugins/eva/contexts/context_product.ml +++ b/src/plugins/eva/contexts/context_product.ml @@ -24,5 +24,5 @@ module Make (L : Abstract_context.S) (R : Abstract_context.S) = struct type t = L.t * R.t let top = (L.top, R.top) let narrow (l, r) (l', r') = - Lattice_bounds.Bottom.zip (L.narrow l l') (R.narrow r r') + Lattice_bounds.Bottom.product (L.narrow l l') (R.narrow r r') end diff --git a/src/plugins/eva/domains/multidim/segmentation.ml b/src/plugins/eva/domains/multidim/segmentation.ml index 3df764821ef6d23e08ce97a2a9a36ec6bf2d0978..88ec2cac45d7a00e4d8f9c6b8c1af10a64bdd513 100644 --- a/src/plugins/eva/domains/multidim/segmentation.ml +++ b/src/plugins/eva/domains/multidim/segmentation.ml @@ -304,14 +304,14 @@ struct let lower_bound ~oracle b1 b2 = if b1 == b2 || eq b1 b2 then `Value b1 else - let+ i1,i2 = Top.zip + let+ i1,i2 = Top.product (lower_integer ~oracle:(oracle Left) b1) (lower_integer ~oracle:(oracle Right) b2) in Const (Integer.min i1 i2) let upper_bound ~oracle b1 b2 = if b1 == b2 || eq b1 b2 then `Value b1 else - let+ i1,i2 = Top.zip + let+ i1,i2 = Top.product (upper_integer ~oracle:(oracle Left) b1) (upper_integer ~oracle:(oracle Right) b2) in Const (Integer.max i1 i2) @@ -510,7 +510,7 @@ struct let hull ~oracle (m : t) : (bound * bound) or_top = let l = m.start and u = last_bound m.segments in - Top.zip (B.lower_const ~oracle l) (B.upper_const ~oracle u) + Top.product (B.lower_const ~oracle l) (B.upper_const ~oracle u) let is_empty_segment ~oracle l u = let open (val (B.operators oracle)) in