diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml index 2269e22db0adeac56affc90149d27def39d767ed..67d3a38cdcaa2bd63c8e1e2d0080e71059169124 100644 --- a/src/plugins/eva/domains/equality/equality_domain.ml +++ b/src/plugins/eva/domains/equality/equality_domain.ml @@ -127,7 +127,7 @@ module Internal = struct let pretty fmt (eqs, _, _) = Equality.Set.pretty fmt eqs - let pretty_debug fmt (eqs, deps, modified) = + let _pretty_debug fmt (eqs, deps, modified) = Format.fprintf fmt "@[<v>@[<hov 2>Eqs: %a@]@.@[<hov 2>Deps: %a@]@.@[<hov 2>Changed: %a@]@]" Equality.Set.pretty eqs Deps.pretty deps @@ -179,19 +179,20 @@ let project (t, _, _) = t module type Context = Abstract.Context.External module type Value = Abstract.Value.External -module Make (Ctx : Context) (Value : Value with type context = Ctx.t) = struct +module Make (Context : Context) (Value : Value with type context = Context.t) = +struct include Internal include Store let get_cvalue = Value.get Main_values.CVal.key - type context = Ctx.t + type context = Context.t type value = Value.t type location = Precise_locs.precise_location type origin - let return_context _ = `Value Ctx.top + let return_context _ = `Value Context.top let reduce_further (equalities, _, _) expr value = let atom = HCE.of_exp expr in diff --git a/src/plugins/eva/domains/equality/equality_domain.mli b/src/plugins/eva/domains/equality/equality_domain.mli index 729e7191ffe585e59ff3ef9a7dcd3f195f8dbf2e..aa35a9e332641fc8cfafabdfbb903fee8caa6aed 100644 --- a/src/plugins/eva/domains/equality/equality_domain.mli +++ b/src/plugins/eva/domains/equality/equality_domain.mli @@ -38,14 +38,10 @@ val project: t -> Equality.Set.t module type Context = Abstract.Context.External module type Value = Abstract.Value.External -module Make (Ctx : Context) (Value : Value with type context = Ctx.t) : sig - include Abstract_domain.S - with type context = Ctx.t - and type value = Value.t - and type location = Precise_locs.precise_location - and type state = t - - val pretty_debug : Format.formatter -> t -> unit -end +module Make (Context : Context) (Value : Value with type context = Context.t) : + Abstract_domain.S with type context = Context.t + and type value = Value.t + and type location = Precise_locs.precise_location + and type state = t val registered : Abstractions.Domain.registered