diff --git a/src/plugins/eva/domains/abstract_domain.ml b/src/plugins/eva/domains/abstract_domain.ml
index 5ce87dae8d64367aa6017d5267195c45aef6a317..3fba964a09919b7915885e47e520968da85e9eb3 100644
--- a/src/plugins/eva/domains/abstract_domain.ml
+++ b/src/plugins/eva/domains/abstract_domain.ml
@@ -514,12 +514,12 @@ module type Leaf = sig
(** The abstract value used by the domain.
It carries the [value] type used by the domain.
See {!Main_values} for some abstract values available in Eva. *)
- val value: value Abstract_value.dependencies
+ val value_dependencies: value Abstract_value.dependencies
(** The abstract location used by the domain.
It carries the [location] type used by the domain.
See {!Main_locations} for the abstract location available in Eva. *)
- val location: location Abstract_location.dependencies
+ val location_dependencies: location Abstract_location.dependencies
end
diff --git a/src/plugins/eva/domains/apron/apron_domain.ml b/src/plugins/eva/domains/apron/apron_domain.ml
index d49c23bc8a43ef64e14e315384a46c9f59ec9a08..2b47a0168f33ebef4a4a11257c5e7995b2bcf7fb 100644
--- a/src/plugins/eva/domains/apron/apron_domain.ml
+++ b/src/plugins/eva/domains/apron/apron_domain.ml
@@ -360,8 +360,8 @@ module Make (Man : Input) = struct
type location = Precise_locs.precise_location
type origin
- let value = Main_values.ival
- let location = Main_locations.ploc
+ let value_dependencies = Main_values.ival
+ let location_dependencies = Main_locations.ploc
let man = Man.manager
let log_category = dkey
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 012cc84fda0d1fbdd758d1142df600f3756a6459..5989aa87bfc229e1f85701ad7cc85777f18b8634 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -187,8 +187,8 @@ module State = struct
type value = Model.value
type location = Model.location
- let value = Main_values.cval
- let location = Main_locations.ploc
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
let top = Model.top, Locals_scoping.bottom ()
let is_included (a, _) (b, _) = Model.is_included a b
diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index a012b6267932bbb0ef8547ac58f23b1bdb3075c9..4349b82595669625eee09b6bed667205575083ee 100644
--- a/src/plugins/eva/domains/domain_builder.ml
+++ b/src/plugins/eva/domains/domain_builder.ml
@@ -115,8 +115,8 @@ module Make_Minimal
type state = Domain.t
type origin
- let value = Abstract_value.Leaf (module Value)
- let location = Abstract_location.Leaf (module Location)
+ let value_dependencies = Abstract_value.Leaf (module Value)
+ let location_dependencies = Abstract_location.Leaf (module Location)
let narrow x _y = `Value x
@@ -229,8 +229,8 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
type state = Domain.t
type origin
- let value = Abstract_value.Leaf (module Main_values.CVal)
- let location = Abstract_location.Leaf (module Main_locations.PLoc)
+ let value_dependencies = Abstract_value.Leaf (module Main_values.CVal)
+ let location_dependencies = Abstract_location.Leaf (module Main_locations.PLoc)
let narrow x _y = `Value x
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index 28846a3982fa21595f3da0326850e9c664332c38..9c7407b2d0138c580d74b96b56252074168718ea 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -533,7 +533,7 @@ end
module Functor = struct
type location = Precise_locs.precise_location
- let location = Main_locations.ploc
+ let location_dependencies = Main_locations.ploc
module Make (V : Abstract.Value.External) = Make (V)
end
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index 96ca72e4f0dd9c70f227071619d03c2490902fd8..0364f4b0f0ffc9c3c1f98fed02d2ec5c7260b1ca 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -1122,8 +1122,8 @@ module D : Abstract_domain.Leaf
type location = Precise_locs.precise_location
type origin
- let value = Main_values.cval
- let location = Main_locations.ploc
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
include G
include Domain_builder.Complete (struct include G let top = empty end)
diff --git a/src/plugins/eva/domains/inout_domain.ml b/src/plugins/eva/domains/inout_domain.ml
index 767419b39a21fd3d6e05f611c793514e716504b8..efcc0bea2fa83a0dd44d5bee81583c8b08811b5f 100644
--- a/src/plugins/eva/domains/inout_domain.ml
+++ b/src/plugins/eva/domains/inout_domain.ml
@@ -211,8 +211,8 @@ module Domain = struct
type location = Precise_locs.precise_location
type origin
- let value = Main_values.cval
- let location = Main_locations.ploc
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
include (LatticeInout: sig
include Datatype.S_with_collections with type t = state
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 0e5e51d466f313ad42f87c07ba5c274df10c1dec..2b2bb6301f28d2a3547714dce4c2c3e10f5314e9 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -365,8 +365,8 @@ struct
let name = "multidim"
- let value = Main_values.cval
- let location = Main_locations.ploc
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
type state = t
type value = Value.t
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 383855045057cdae5c22828b17ccfe74cab9b1d3..950dc8745b371c643e11a8df1865e97798e22982 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1616,8 +1616,8 @@ module Domain = struct
type location = Precise_locs.precise_location
type origin
- let value = Main_values.cval
- let location = Main_locations.ploc
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
let top_value = `Value (Cvalue.V.top, None), Alarmset.all
diff --git a/src/plugins/eva/domains/offsm_domain.ml b/src/plugins/eva/domains/offsm_domain.ml
index e0f66bc210d12698fb382a027c055d68d798d999..6714d6986b29bda399e5ccb49aa039ef05d9b8bc 100644
--- a/src/plugins/eva/domains/offsm_domain.ml
+++ b/src/plugins/eva/domains/offsm_domain.ml
@@ -101,8 +101,8 @@ module D : Abstract_domain.Leaf
type location = Precise_locs.precise_location
type origin
- let value = Abstract_value.Leaf (module Offsm_value.Offsm)
- let location = Main_locations.ploc
+ let value_dependencies = Abstract_value.Leaf (module Offsm_value.Offsm)
+ let location_dependencies = Main_locations.ploc
include (Memory: sig
include Datatype.S_with_collections with type t = state
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index ea6b2e3669621d05dc9aba4bb4ea10307472899f..deb6d926511f5d590daef40d9b830084ee78d1a5 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -194,8 +194,8 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
type location = Precise_locs.precise_location
type origin
- let value = Abstract_value.Leaf (module Value)
- let location = Main_locations.ploc
+ let value_dependencies = Abstract_value.Leaf (module Value)
+ let location_dependencies = Main_locations.ploc
let log_category = Self.register_category ("d-" ^ Info.name)
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index d4a291e1ca570b3e31545ff20772883f187afac3..c174803290531a6985cf538763f9483be7edd2ad 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -464,8 +464,8 @@ module D : Abstract_domain.Leaf
type location = Precise_locs.precise_location
type origin
- let value = Main_values.cval
- let location = Main_locations.ploc
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
include (Memory: sig
include Datatype.S_with_collections with type t = state
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index 8c84df60c45755e904313bc129af8b0ce041bfdc..4c37d351ce496021ba57d010b0577c792356c66f 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -301,8 +301,8 @@ module Domain = struct
type location = Precise_locs.precise_location
type origin
- let value = Main_values.cval
- let location = Main_locations.ploc
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
include (LatticeTaint: sig
include Datatype.S_with_collections with type t = state
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index 276603c4eaf3cdc527c5363f90077e0f50e1fda5..cda82de061d84559cc90ea3d4fd7426ee43c62ea 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -1089,8 +1089,8 @@ module D = struct
type location = Precise_locs.precise_location
type origin
- let value = Main_values.cval
- let location = Main_locations.ploc
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
include (Traces: sig
include Datatype.S_with_collections with type t = state
diff --git a/src/plugins/eva/engine/abstractions.ml b/src/plugins/eva/engine/abstractions.ml
index 2ebbb6c4b18680e22e8af28792dcbef4a7c49399..ef09af89e6d91a9a4fafb5035a67f30bb641acaa 100644
--- a/src/plugins/eva/engine/abstractions.ml
+++ b/src/plugins/eva/engine/abstractions.ml
@@ -306,7 +306,7 @@ module Domain = struct
fixed locations dependencies. *)
module type Functor = sig
type location
- val location: location Abstract_location.dependencies
+ val location_dependencies: location Abstract_location.dependencies
module Make (V : Abstract.Value.External) : sig
include Abstract_domain.S
with type value = V.t and type location = location
@@ -434,7 +434,7 @@ module Domain = struct
let lifted : (v, l) structured_domain =
match registered.abstraction with
| Functor (module Functor) ->
- let locs = Location.outline Functor.location in
+ let locs = Location.outline Functor.location_dependencies in
let eq_loc = Location.dec_eq locs Loc.structure in
let module D = Functor.Make (Val) in
begin match eq_loc with
@@ -450,8 +450,8 @@ module Domain = struct
(module Domain_lift.Make (D) (Val) (Loc))
end
| Domain (module D) ->
- let loc_deps = Location.outline D.location in
- let val_deps = Value.outline D.value in
+ let loc_deps = Location.outline D.location_dependencies in
+ let val_deps = Value.outline D.value_dependencies in
let eq_loc = Location.dec_eq loc_deps Loc.structure in
let eq_val = Value.dec_eq val_deps Val.structure in
begin match eq_val, eq_loc with
@@ -524,10 +524,10 @@ module Domain = struct
let add_values values (registered, _) =
match registered.abstraction with
| Domain (module Domain) ->
- Value.fold add_value Domain.value values |>
- Location.fold_values add_value Domain.location
+ Value.fold add_value Domain.value_dependencies values |>
+ Location.fold_values add_value Domain.location_dependencies
| Functor (module F) ->
- Location.fold_values add_value F.location values
+ Location.fold_values add_value F.location_dependencies values
in
List.fold_left add_values Value.init domains |>
Value.make_interactive
@@ -535,11 +535,11 @@ module Domain = struct
let module V = (val Value.assert_not_unit values) in
let locations =
let init : V.t Location.structured = Location.init (module V) in
- let add_loc = Location.{ folder = add } in
+ let add = Location.{ folder = add } in
let add_locations locs (registered, _) =
match registered.abstraction with
- | Domain (module D) -> Location.fold add_loc D.location locs
- | Functor (module D) -> Location.fold add_loc D.location locs
+ | Domain (module D) -> Location.fold add D.location_dependencies locs
+ | Functor (module D) -> Location.fold add D.location_dependencies locs
in
List.fold_left add_locations init domains |>
Location.make_interactive
diff --git a/src/plugins/eva/engine/abstractions.mli b/src/plugins/eva/engine/abstractions.mli
index 55ffe2c2f624b68955ce41a12d58bdd564fb4d03..395c1000004fd1daa3e1da233835ac06ded88787 100644
--- a/src/plugins/eva/engine/abstractions.mli
+++ b/src/plugins/eva/engine/abstractions.mli
@@ -53,7 +53,7 @@ module Domain : sig
fixed locations dependencies. *)
module type Functor = sig
type location
- val location: location Abstract_location.dependencies
+ val location_dependencies: location Abstract_location.dependencies
module Make (V : Abstract.Value.External) : sig
include Abstract_domain.S
with type value = V.t and type location = location