diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml index 9d0299b703635aeb4146832b5564dc7638a6d753..ddf7bae272b9a77f854c3f3adac277e14ade6602 100644 --- a/src/plugins/value/domains/equality/equality_domain.ml +++ b/src/plugins/value/domains/equality/equality_domain.ml @@ -123,9 +123,6 @@ module Internal = struct let log_category = dkey - type equalities = Equality.Set.t - let project (t, _, _) = t - let pretty fmt (eqs, _, _) = Equality.Set.pretty fmt eqs let pretty_debug fmt (eqs, deps, modified) = @@ -170,6 +167,10 @@ end module Store = Domain_builder.Complete (Internal) +type t = Internal.t +let key = Store.key +let project (t, _, _) = t + (* ------------------------- Abstract Domain -------------------------------- *) diff --git a/src/plugins/value/domains/equality/equality_domain.mli b/src/plugins/value/domains/equality/equality_domain.mli index 7adbbb6f9e6e6e267581c54e845c2e79271e92e1..b903b6e82d0b3e4a8112ac574d4307bb32bab492 100644 --- a/src/plugins/value/domains/equality/equality_domain.mli +++ b/src/plugins/value/domains/equality/equality_domain.mli @@ -31,12 +31,14 @@ type call_init_state = | ISEmpty (** completely empty state, without impact on Memexec. *) +type t +val key: t Abstract_domain.key +val project: t -> Equality.Set.t + module Make (Value : Abstract.Value.External) : sig include Abstract_domain.Leaf with type value = Value.t and type location = Precise_locs.precise_location + and type state = t val pretty_debug : Format.formatter -> t -> unit - - type equalities - val project : t -> equalities end