diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml index 204ad8aa11e5eeea839c306f7343033f456b7f88..46c8138c810a831fb0e3ebf926354588849c5788 100644 --- a/src/kernel_services/abstract_interp/map_lattice.ml +++ b/src/kernel_services/abstract_interp/map_lattice.ml @@ -392,8 +392,7 @@ module Make_MapSet_Lattice let is_included t1 t2 = match t1, t2 with - | Top (s1, o1), Top (s2, o2) -> - KSet.is_included s1 s2 && Origin.is_included o1 o2 + | Top (s1, _), Top (s2, _) -> KSet.is_included s1 s2 | Map _, Top (KSet.Top, _) -> true | Map m, Top (KSet.Set s, _) -> KVMap.for_all (fun k _ -> KSet.O.mem k s) m | Top _, Map _ -> false diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml index 422fc364d378f93c2cfa452560972958ea929cd2..357ebfd681a2f55cc8dd3ab93b61e9545dac4988 100644 --- a/src/kernel_services/abstract_interp/origin.ml +++ b/src/kernel_services/abstract_interp/origin.ml @@ -119,8 +119,6 @@ let join t1 t2 = | Well, _ | _, Well -> Well | Origin o1, Origin o2 -> if o1.id <= o2.id then t1 else t2 -let is_included = equal - (* For each garbled mix origin, keep track of: - the number of writes (according to [register_write] below), i.e. the number diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli index a5d1ce6566cad15266083eafe041f6de6f5bf328..bb8cdc57192bd5ebf3e2932f41bbb66f10f855ad 100644 --- a/src/kernel_services/abstract_interp/origin.mli +++ b/src/kernel_services/abstract_interp/origin.mli @@ -53,7 +53,6 @@ val pretty_as_reason: Format.formatter -> t -> unit val descr: t -> string val join: t -> t -> t -val is_included: t -> t -> bool (** Records the write of an imprecise value of the given bases, with the given origin.