From b17d337529d487fecd87b1c752f922ae34a30110 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 17 Sep 2021 16:44:19 +0200
Subject: [PATCH] [Eva] api: Exports the key of the equality domain.
---
src/plugins/value/domains/equality/equality_domain.ml | 7 ++++---
src/plugins/value/domains/equality/equality_domain.mli | 8 +++++---
2 files changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 9d0299b7036..ddf7bae272b 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 7adbbb6f9e6..b903b6e82d0 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
--
GitLab