diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml index afc8590b20d27070a5f7842c12c4dc86fb642035..91f61c4ddc07b1d34bb1ec56f8221d70145682bd 100644 --- a/src/kernel_services/abstract_interp/locations.ml +++ b/src/kernel_services/abstract_interp/locations.ml @@ -271,16 +271,8 @@ module Location_Bytes = struct let contains_addresses_of_any_locals = let f base _offsets = Base.is_any_formal_or_local base in - let projection _base = Ival.top in let cache = Hptmap_sig.PersistentCache "loc_top_any_locals" in - let cached_f = - cached_fold - ~cache - ~f - ~projection - ~joiner:(||) - ~empty:false - in + let cached_f = cached_fold ~cache ~f ~joiner:(||) ~empty:false in fun loc -> try cached_f loc diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli index 081c430c0ed2cba6c6342f95ab7290889ba7abba..8e953c90d33e7688179e7c4fb0e8813001ae4c37 100644 --- a/src/kernel_services/abstract_interp/locations.mli +++ b/src/kernel_services/abstract_interp/locations.mli @@ -151,7 +151,6 @@ module Location_Bytes : sig val cached_fold: cache:Hptmap_sig.cache_type -> f:(Base.t -> Ival.t -> 'a) -> - projection:(Base.t -> Ival.t) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a (** Cached version of [fold_i], for advanced users *) @@ -289,7 +288,6 @@ module Zone : sig val cached_fold : cache:Hptmap_sig.cache_type -> f:(Base.t -> Int_Intervals.t -> 'b) -> - projection:(Base.t -> Int_Intervals.t) -> joiner:('b -> 'b -> 'b) -> empty:'b -> t -> 'b val fold2_join_heterogeneous: diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml index 713ad30918a9507f8649def90b1a3bd815e0d644..d2e1cb5b28c7824e34c40216726b6c719ef8be0e 100644 --- a/src/kernel_services/abstract_interp/map_lattice.ml +++ b/src/kernel_services/abstract_interp/map_lattice.ml @@ -81,8 +81,7 @@ module type MapSet_Lattice = sig val fold : (key -> v -> 'a -> 'a) -> t -> 'a -> 'a val cached_fold: cache:Hptmap_sig.cache_type -> - f:(key -> v -> 'a) -> - projection:(key -> v) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a + f:(key -> v -> 'a) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a val for_all: (key -> v -> bool) -> t -> bool val exists: (key -> v -> bool) -> t -> bool val pretty_debug : Format.formatter -> t -> unit @@ -436,15 +435,12 @@ module Make_MapSet_Lattice | Top (s, _) -> KSet.fold (fun x acc -> f x Value.top acc) s acc | Map m -> KVMap.fold f m acc - let cached_fold ~cache ~f ~projection ~joiner ~empty = + let cached_fold ~cache ~f ~joiner ~empty = let folded_f = KVMap.cached_fold ~cache ~f ~joiner ~empty in function | Top (KSet.Top, _) -> raise Abstract_interp.Error_Top | Top (KSet.Set s, _) -> - let f_base base acc = - let total_itvs = projection base in - joiner (f base total_itvs) acc - in + let f_base base acc = joiner (f base Value.top) acc in KSet.O.fold f_base s empty | Map m -> folded_f m diff --git a/src/kernel_services/abstract_interp/map_lattice.mli b/src/kernel_services/abstract_interp/map_lattice.mli index 1ef2068c67b7212b05c03ee0b68f2efa4158c13f..20d149828f25dbb0898dd5d1eb9033e74acbf1ea 100644 --- a/src/kernel_services/abstract_interp/map_lattice.mli +++ b/src/kernel_services/abstract_interp/map_lattice.mli @@ -126,8 +126,7 @@ module type MapSet_Lattice = sig val cached_fold: cache:Hptmap_sig.cache_type -> - f:(key -> v -> 'a) -> - projection:(key -> v) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a + f:(key -> v -> 'a) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a (** [for_all p t] checks if all binding of [t] satisfy [p] . Always false if [t] is top. *) diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml index de69304cdf86af51a3b79d44b076cb2868bafd6d..730527d6683647f52e77f1399b1cc961e5357cf2 100644 --- a/src/plugins/from/functionwise.ml +++ b/src/plugins/from/functionwise.ml @@ -65,10 +65,9 @@ module To_Use = struct else Zone.bottom in let joiner = Zone.join in - let projection _ = Int_Intervals.top in let cache = Hptmap_sig.TemporaryCache "from cleanup" in let zone_substitution = - Zone.cached_fold ~cache ~f ~joiner ~empty:Zone.bottom ~projection + Zone.cached_fold ~cache ~f ~joiner ~empty:Zone.bottom in let zone_substitution x = try