diff --git a/src/plugins/eva/domains/apron/apron_domain.ml b/src/plugins/eva/domains/apron/apron_domain.ml
index 691980d0ed5286e0fc9884f70bed6b267281cc28..ec320503fdf6537338066f6f4f02b6c7639838fc 100644
--- a/src/plugins/eva/domains/apron/apron_domain.ml
+++ b/src/plugins/eva/domains/apron/apron_domain.ml
@@ -428,7 +428,6 @@ module Make (Man : Input) = struct
let s = Abstract1.meet man s1 s2 in
if Abstract1.is_bottom man s then `Bottom else `Value s
- include Domain_builder.No_context
include Domain_builder.Complete
(struct
include D
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 888a0d0cafe13bb0de1369bcab6b90df71035366..1fd21a94a0c1b556401469c22e177403f5a0e26d 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -32,7 +32,10 @@ module State = struct
let value_dependencies = Main_values.cval
let location_dependencies = Main_locations.ploc
- include Domain_builder.No_context
+
+ type context = unit
+ let context_dependencies = Abstract_context.Leaf (module Unit_context)
+ let return_context _ = `Value ()
let log_category = Self.dkey_cvalue_domain
diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index c67308531fe0403624530bc9c2d4b6aa140ebe27..c7324a89dbc5d834c3699f5aeb287ce80a26c297 100644
--- a/src/plugins/eva/domains/domain_builder.ml
+++ b/src/plugins/eva/domains/domain_builder.ml
@@ -36,6 +36,10 @@ end
module type LeafDomain = sig
type t
+ type context = unit
+ val context_dependencies: context Abstract_context.dependencies
+ val return_context: t -> context or_bottom
+
val backward_location: t -> lval -> typ -> 'loc -> 'v -> ('loc * 'v) or_bottom
val reduce_further: t -> exp -> 'v -> (exp * 'v) list
@@ -66,16 +70,11 @@ module type LeafDomain = sig
end
+module Complete (Domain: InputDomain) = struct
-module No_context = struct
type context = unit
let context_dependencies = Abstract_context.Leaf (module Unit_context)
let return_context _ = `Value ()
-end
-
-
-
-module Complete (Domain: InputDomain) = struct
let backward_location _state _lval _typ loc value = `Value (loc, value)
let reduce_further _state _expr _value = []
@@ -119,7 +118,6 @@ let simplify_call call =
module Make_Minimal
- (Context : Abstract_context.Leaf)
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Simpler_domains.Minimal)
@@ -129,14 +127,11 @@ module Make_Minimal
let log_category = Self.register_category ("d-" ^ name)
- type context = Context.t
type value = Value.t
type location = Location.location
type state = Domain.t
type origin
- let return_context _ = `Value Context.top
- let context_dependencies = Abstract_context.Leaf (module Context)
let value_dependencies = Abstract_value.Leaf (module Value)
let location_dependencies = Abstract_location.Leaf (module Location)
@@ -181,14 +176,13 @@ end
module Complete_Minimal
- (Context : Abstract_context.Leaf)
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Simpler_domains.Minimal)
= struct
module D = struct
- include Make_Minimal (Context) (Value) (Location) (Domain)
+ include Make_Minimal (Value) (Location) (Domain)
include
(Datatype.Make_with_collections
@@ -213,7 +207,6 @@ end
module Complete_Minimal_with_datatype
- (Context : Abstract_context.Leaf)
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Minimal_with_datatype)
@@ -221,7 +214,7 @@ module Complete_Minimal_with_datatype
module D = struct
- include Make_Minimal (Context) (Value) (Location) (Domain)
+ include Make_Minimal (Value) (Location) (Domain)
include
(Datatype.With_collections
@@ -254,8 +247,6 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
type state = Domain.t
type origin
- include No_context
-
let value_dependencies = Abstract_value.Leaf (module Main_values.CVal)
let location_dependencies = Abstract_location.Leaf (module Main_locations.PLoc)
diff --git a/src/plugins/eva/domains/domain_builder.mli b/src/plugins/eva/domains/domain_builder.mli
index 568c5509ec260a8d0441588a6b234d36956e6b2b..7f24bb4a8c90a99eab5f99d03b6ccae3dac2c7c2 100644
--- a/src/plugins/eva/domains/domain_builder.mli
+++ b/src/plugins/eva/domains/domain_builder.mli
@@ -40,6 +40,10 @@ end
module type LeafDomain = sig
type t
+ type context = unit
+ val context_dependencies: context Abstract_context.dependencies
+ val return_context: t -> context or_bottom
+
val backward_location: t -> lval -> typ -> 'loc -> 'v -> ('loc * 'v) or_bottom
val reduce_further: t -> exp -> 'v -> (exp * 'v) list
@@ -69,31 +73,23 @@ module type LeafDomain = sig
val key: t Abstract_domain.key
end
-module No_context : sig
- type context = unit
- val context_dependencies : context Abstract_context.dependencies
- val return_context : 'a -> context Eval.or_bottom
-end
-
(** Automatically builds some functions of an abstract domain. *)
module Complete (Domain: InputDomain) : LeafDomain with type t := Domain.t
module Complete_Minimal
- (Context : Abstract_context.Leaf)
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Simpler_domains.Minimal)
- : Abstract_domain.Leaf with type context = Context.t
+ : Abstract_domain.Leaf with type context = unit
and type value = Value.t
and type location = Location.location
and type state = Domain.t
module Complete_Minimal_with_datatype
- (Context : Abstract_context.Leaf)
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Simpler_domains.Minimal_with_datatype)
- : Abstract_domain.Leaf with type context = Context.t
+ : Abstract_domain.Leaf with type context = unit
and type value = Value.t
and type location = Location.location
and type state = Domain.t
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index a1e82cd863a374c06b9f42183ddf3ce53785e2e3..4fc078eb9d22f2fe0b19235dae08aa01cae1daee 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -1125,7 +1125,6 @@ module D : Abstract_domain.Leaf
include G
include Domain_builder.Complete (struct include G let top = empty end)
- include Domain_builder.No_context
let log_category = dkey
diff --git a/src/plugins/eva/domains/inout_domain.ml b/src/plugins/eva/domains/inout_domain.ml
index 728c892b7d474eb4d8c457f6965bfaf815556468..db4680480a4b074883a7880ed930c2a71a9c64b7 100644
--- a/src/plugins/eva/domains/inout_domain.ml
+++ b/src/plugins/eva/domains/inout_domain.ml
@@ -220,7 +220,6 @@ module Domain = struct
end)
include Domain_builder.Complete (LatticeInout)
- include Domain_builder.No_context
let log_category = Self.register_category "d-inout"
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 92f546a13bf524ac6ef70c9a341f7870fc3c3f24..c34c84acc994dd8348aba9af923a7058a7d03efb 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -664,7 +664,6 @@ module Domain =
struct
include DomainLattice
include Domain_builder.Complete (DomainLattice)
- include Domain_builder.No_context
(* Eva Queries *)
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index eab6d98444aee65992d5eee311244f09d283ab68..33be2920a29172dabe0ebf5c32eec98d07df2b46 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1600,7 +1600,6 @@ module Domain = struct
include State
include Domain_builder.Complete (State)
- include Domain_builder.No_context
type value = Cvalue.V.t
type location = Precise_locs.precise_location
diff --git a/src/plugins/eva/domains/offsm_domain.ml b/src/plugins/eva/domains/offsm_domain.ml
index 652cca15035b342d3859c95857ec38aab88d87fb..806d306d6f70e73bae0f833f0f429fb9999f4e18 100644
--- a/src/plugins/eva/domains/offsm_domain.ml
+++ b/src/plugins/eva/domains/offsm_domain.ml
@@ -110,7 +110,6 @@ module D : Abstract_domain.Leaf
end)
include Domain_builder.Complete (Memory)
- include Domain_builder.No_context
let log_category = dkey
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index d0356313438ab57515f33950a74e0d50f9767ddc..d2c81be458b371f7f320c566d0d77ae53d6b2088 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -188,7 +188,6 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
include M
include Domain_builder.Complete (M)
- include Domain_builder.No_context
type state = t
type value = Value.t
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index 1a5ebf09887036734c48e56822c037a0cfe80b11..0719ce81c897066c3a6302ec334dc68d85ae911a 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -472,7 +472,6 @@ module D : Abstract_domain.Leaf
end)
include Domain_builder.Complete (Memory)
- include Domain_builder.No_context
let log_category = dkey
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index e0b0d4f3c07f1fd585db4313514983790a8ea1d4..d20a13adf8ab68cf6ef4181c5b0d7bfe835b93a0 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -310,7 +310,6 @@ module Domain = struct
end)
include Domain_builder.Complete (LatticeTaint)
- include Domain_builder.No_context
include QueriesTaint
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index d631c13e3585b5892a04cf0ca55c2284926884a9..53eb03a0032d1c1111ba34594b3f3ea6f61b3aaf 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -1089,7 +1089,6 @@ module D = struct
type location = Precise_locs.precise_location
type origin
- include Domain_builder.No_context
let value_dependencies = Main_values.cval
let location_dependencies = Main_locations.ploc
diff --git a/src/plugins/eva/domains/unit_domain.ml b/src/plugins/eva/domains/unit_domain.ml
index 378f0437b3046ae3b56af1dd80f9fc757b15860b..0d05955f1901bb0085d5a7a72dff96f0ee10ca09 100644
--- a/src/plugins/eva/domains/unit_domain.ml
+++ b/src/plugins/eva/domains/unit_domain.ml
@@ -25,7 +25,6 @@ let log_key = Self.register_category "unit-domain"
module Static = struct
module D = struct
include Datatype.Unit
- include Domain_builder.No_context
type state = t
let name = "unit"