Skip to content
Snippets Groups Projects
Commit e026c8cc authored by David Bühler's avatar David Bühler
Browse files

[Eva] Removes module type Abstract.Interface, which is exactly Structure.External.

parent 6df6bd4c
No related branches found
No related tags found
No related merge requests found
...@@ -20,17 +20,9 @@ ...@@ -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 (** Partition of the abstract states, computed for each node by the
dataflow analysis. *) dataflow analysis. *)
module Make module Make (Domain : Abstract.Domain.External)
(Domain : Domain)
= struct = struct
module Index = Hashtbl.Make (Cvalue_domain.Subpart) module Index = Hashtbl.Make (Cvalue_domain.Subpart)
......
...@@ -30,14 +30,7 @@ ...@@ -30,14 +30,7 @@
Partitioning index relies on an heuristics on the cvalue domain, Partitioning index relies on an heuristics on the cvalue domain,
and is very inefficient without it. *) and is very inefficient without it. *)
module type Domain = sig module Make (Domain: Abstract.Domain.External) : 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
type t type t
(** Creates an empty index. *) (** Creates an empty index. *)
......
...@@ -20,15 +20,6 @@ ...@@ -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 Value = struct
module V = struct module V = struct
...@@ -46,6 +37,7 @@ module Value = struct ...@@ -46,6 +37,7 @@ module Value = struct
include Internal include Internal
include Structure.External with type t := t include Structure.External with type t := t
and type 'a key := 'a key and type 'a key := 'a key
and type 'a data := 'a data
end end
end end
...@@ -66,6 +58,7 @@ module Location = struct ...@@ -66,6 +58,7 @@ module Location = struct
include Internal include Internal
include Structure.External with type t := location include Structure.External with type t := location
and type 'a key := 'a key and type 'a key := 'a key
and type 'a data := 'a data
end end
end end
...@@ -86,6 +79,7 @@ module Domain = struct ...@@ -86,6 +79,7 @@ module Domain = struct
include Internal include Internal
include Structure.External with type t := t include Structure.External with type t := t
and type 'a key := 'a key and type 'a key := 'a key
and type 'a data := 'a data
val get_cvalue: (t -> Cvalue.Model.t) option val get_cvalue: (t -> Cvalue.Model.t) option
val get_cvalue_or_top: t -> Cvalue.Model.t val get_cvalue_or_top: t -> Cvalue.Model.t
......
...@@ -33,28 +33,6 @@ ...@@ -33,28 +33,6 @@
Note that their behavior is undefined if an abstraction contains Note that their behavior is undefined if an abstraction contains
several times the same leaf module. *) 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. (** Key and structure for abstract values.
See {structure.mli} for more details. *) See {structure.mli} for more details. *)
module Value : sig module Value : sig
...@@ -69,8 +47,9 @@ module Value : sig ...@@ -69,8 +47,9 @@ module Value : sig
module type External = sig module type External = sig
include Internal include Internal
include Interface with type t := t include Structure.External with type t := t
and type 'a key := 'a key and type 'a key := 'a key
and type 'a data := 'a data
end end
end end
...@@ -88,8 +67,9 @@ module Location : sig ...@@ -88,8 +67,9 @@ module Location : sig
module type External = sig module type External = sig
include Internal include Internal
include Interface with type t := location include Structure.External with type t := location
and type 'a key := 'a key and type 'a key := 'a key
and type 'a data := 'a data
end end
end end
...@@ -107,8 +87,9 @@ module Domain : sig ...@@ -107,8 +87,9 @@ module Domain : sig
module type External = sig module type External = sig
include Internal include Internal
include Interface with type t := t include Structure.External with type t := t
and type 'a key := 'a key and type 'a key := 'a key
and type 'a data := 'a data
(** Special accessors for the main cvalue domain. *) (** Special accessors for the main cvalue domain. *)
val get_cvalue: (t -> Cvalue.Model.t) option val get_cvalue: (t -> Cvalue.Model.t) option
......
...@@ -143,6 +143,7 @@ end ...@@ -143,6 +143,7 @@ end
module type External = sig module type External = sig
type t type t
type 'a key type 'a key
type 'a data
val mem : 'a key -> bool val mem : 'a key -> bool
val get : 'a key -> (t -> 'a) option val get : 'a key -> (t -> 'a) option
val set : 'a key -> 'a -> t -> t val set : 'a key -> 'a -> t -> t
......
...@@ -89,8 +89,22 @@ end ...@@ -89,8 +89,22 @@ end
module type External = sig module type External = sig
type t type t
type 'a key type 'a key
type 'a data
(** Tests whether a key belongs to the module. *)
val mem : 'a key -> bool 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 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 val set : 'a key -> 'a -> t -> t
end end
...@@ -100,3 +114,4 @@ module Open ...@@ -100,3 +114,4 @@ module Open
(Data : Internal with type 'a structure := 'a Shape.structure) (Data : Internal with type 'a structure := 'a Shape.structure)
: External with type t := Data.t : External with type t := Data.t
and type 'a key := 'a Shape.key and type 'a key := 'a Shape.key
and type 'a data := 'a Shape.data
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment