diff --git a/src/plugins/value/partitioning/partitioning_index.ml b/src/plugins/value/partitioning/partitioning_index.ml
index 431e0f05ebb90a694285c0931bc1804965f15d80..29660a56c04996048db544b2c20a9c8ed2136d7a 100644
--- a/src/plugins/value/partitioning/partitioning_index.ml
+++ b/src/plugins/value/partitioning/partitioning_index.ml
@@ -20,17 +20,9 @@
(* *)
(**************************************************************************)
-module type Domain = sig
- include Abstract_domain.Lattice
- include Datatype.S_with_collections with type t = state
- include Abstract.Interface with type t := state
- and type 'a key := 'a Abstract_domain.key
-end
-
(** Partition of the abstract states, computed for each node by the
dataflow analysis. *)
-module Make
- (Domain : Domain)
+module Make (Domain : Abstract.Domain.External)
= struct
module Index = Hashtbl.Make (Cvalue_domain.Subpart)
diff --git a/src/plugins/value/partitioning/partitioning_index.mli b/src/plugins/value/partitioning/partitioning_index.mli
index 7d119f87db238a99bcdd3f65e3c24874517d7b68..21bdef9d1fd92e6a68ffb8534de8e8baebdf5d96 100644
--- a/src/plugins/value/partitioning/partitioning_index.mli
+++ b/src/plugins/value/partitioning/partitioning_index.mli
@@ -30,14 +30,7 @@
Partitioning index relies on an heuristics on the cvalue domain,
and is very inefficient without it. *)
-module type Domain = sig
- include Abstract_domain.Lattice
- include Datatype.S_with_collections with type t = state
- include Abstract.Interface with type t := state
- and type 'a key := 'a Abstract_domain.key
-end
-
-module Make (Domain: Domain) : sig
+module Make (Domain: Abstract.Domain.External) : sig
type t
(** Creates an empty index. *)
diff --git a/src/plugins/value/utils/abstract.ml b/src/plugins/value/utils/abstract.ml
index 1b5be7c02b3367f62d1077fdaf654a2e5ce0cff3..266de82c9fb0eecc1cbf684d3a98fdf0c61c512a 100644
--- a/src/plugins/value/utils/abstract.ml
+++ b/src/plugins/value/utils/abstract.ml
@@ -20,15 +20,6 @@
(* *)
(**************************************************************************)
-(** External interface of an abstraction, built by {!Structure.Open}. *)
-module type Interface = sig
- type t
- type 'a key
- val mem : 'a key -> bool
- val get : 'a key -> (t -> 'a) option
- val set : 'a key -> 'a -> t -> t
-end
-
module Value = struct
module V = struct
@@ -46,6 +37,7 @@ module Value = struct
include Internal
include Structure.External with type t := t
and type 'a key := 'a key
+ and type 'a data := 'a data
end
end
@@ -66,6 +58,7 @@ module Location = struct
include Internal
include Structure.External with type t := location
and type 'a key := 'a key
+ and type 'a data := 'a data
end
end
@@ -86,6 +79,7 @@ module Domain = struct
include Internal
include Structure.External with type t := t
and type 'a key := 'a key
+ and type 'a data := 'a data
val get_cvalue: (t -> Cvalue.Model.t) option
val get_cvalue_or_top: t -> Cvalue.Model.t
diff --git a/src/plugins/value/utils/abstract.mli b/src/plugins/value/utils/abstract.mli
index 087cae69ffcb7aed9c473009cd4b25e244b5a41c..1e27948b1c37c0546a37129c71fb4d92d8636232 100644
--- a/src/plugins/value/utils/abstract.mli
+++ b/src/plugins/value/utils/abstract.mli
@@ -33,28 +33,6 @@
Note that their behavior is undefined if an abstraction contains
several times the same leaf module. *)
-(** External interface of an abstraction, built by {!Structure.Open}. *)
-module type Interface = sig
- type t
- type 'a key
-
- (** Tests whether a key belongs to the module. *)
- val mem : 'a key -> bool
-
- (** For a key of type [k key]:
- - if the values of type [t] contain a subpart of type [k] from a module
- identified by the key, then [get key] returns an accessor for it.
- - otherwise, [get key] returns None. *)
- val get : 'a key -> (t -> 'a) option
-
- (** For a key of type [k key]:
- - if the values of type [t] contain a subpart of type [k] from a module
- identified by the key, then [set key v t] returns the value [t] in which
- this subpart has been replaced by [v].
- - otherwise, [set key _] is the identity function. *)
- val set : 'a key -> 'a -> t -> t
-end
-
(** Key and structure for abstract values.
See {structure.mli} for more details. *)
module Value : sig
@@ -69,8 +47,9 @@ module Value : sig
module type External = sig
include Internal
- include Interface with type t := t
- and type 'a key := 'a key
+ include Structure.External with type t := t
+ and type 'a key := 'a key
+ and type 'a data := 'a data
end
end
@@ -88,8 +67,9 @@ module Location : sig
module type External = sig
include Internal
- include Interface with type t := location
- and type 'a key := 'a key
+ include Structure.External with type t := location
+ and type 'a key := 'a key
+ and type 'a data := 'a data
end
end
@@ -107,8 +87,9 @@ module Domain : sig
module type External = sig
include Internal
- include Interface with type t := t
- and type 'a key := 'a key
+ include Structure.External with type t := t
+ and type 'a key := 'a key
+ and type 'a data := 'a data
(** Special accessors for the main cvalue domain. *)
val get_cvalue: (t -> Cvalue.Model.t) option
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index c16589366c54e22f4df847384f290bb8ad04e472..0df7cdad3ee0f80f55cc407f732488369bcdd097 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -143,6 +143,7 @@ end
module type External = sig
type t
type 'a key
+ type 'a data
val mem : 'a key -> bool
val get : 'a key -> (t -> 'a) option
val set : 'a key -> 'a -> t -> t
diff --git a/src/plugins/value/utils/structure.mli b/src/plugins/value/utils/structure.mli
index e98ec0c7b0531d692f30dcd93b57b90e4dfef6b6..942ffb87331c5d7625ff1db55559cefcee2e7602 100644
--- a/src/plugins/value/utils/structure.mli
+++ b/src/plugins/value/utils/structure.mli
@@ -89,8 +89,22 @@ end
module type External = sig
type t
type 'a key
+ type 'a data
+
+ (** Tests whether a key belongs to the module. *)
val mem : 'a key -> bool
+
+ (** For a key of type [k key]:
+ - if the values of type [t] contain a subpart of type [k] from a module
+ identified by the key, then [get key] returns an accessor for it.
+ - otherwise, [get key] returns None. *)
val get : 'a key -> (t -> 'a) option
+
+ (** For a key of type [k key]:
+ - if the values of type [t] contain a subpart of type [k] from a module
+ identified by the key, then [set key v t] returns the value [t] in which
+ this subpart has been replaced by [v].
+ - otherwise, [set key _] is the identity function. *)
val set : 'a key -> 'a -> t -> t
end
@@ -100,3 +114,4 @@ module Open
(Data : Internal with type 'a structure := 'a Shape.structure)
: External with type t := Data.t
and type 'a key := 'a Shape.key
+ and type 'a data := 'a Shape.data