From d8f75dcb771c30f5bb52699f143578a3a10f3150 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime2.jacquemin@gmail.com>
Date: Tue, 4 Jul 2023 09:38:03 +0200
Subject: [PATCH] [Eva] More explicit names for domain dependencies
---
src/plugins/eva/domains/abstract_domain.ml | 4 ++--
src/plugins/eva/domains/apron/apron_domain.ml | 4 ++--
.../eva/domains/cvalue/cvalue_domain.ml | 4 ++--
src/plugins/eva/domains/domain_builder.ml | 8 ++++----
.../eva/domains/equality/equality_domain.ml | 2 +-
.../eva/domains/gauges/gauges_domain.ml | 4 ++--
src/plugins/eva/domains/inout_domain.ml | 4 ++--
.../eva/domains/multidim/multidim_domain.ml | 4 ++--
src/plugins/eva/domains/octagons.ml | 4 ++--
src/plugins/eva/domains/offsm_domain.ml | 4 ++--
src/plugins/eva/domains/simple_memory.ml | 4 ++--
src/plugins/eva/domains/symbolic_locs.ml | 4 ++--
src/plugins/eva/domains/taint_domain.ml | 4 ++--
src/plugins/eva/domains/traces_domain.ml | 4 ++--
src/plugins/eva/engine/abstractions.ml | 20 +++++++++----------
src/plugins/eva/engine/abstractions.mli | 2 +-
16 files changed, 40 insertions(+), 40 deletions(-)
diff --git a/src/plugins/eva/domains/abstract_domain.ml b/src/plugins/eva/domains/abstract_domain.ml
index 5ce87dae8d6..3fba964a099 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 d49c23bc8a4..2b47a0168f3 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 012cc84fda0..5989aa87bfc 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 a012b626793..4349b825956 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 28846a3982f..9c7407b2d01 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 96ca72e4f0d..0364f4b0f0f 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 767419b39a2..efcc0bea2fa 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 0e5e51d466f..2b2bb6301f2 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 38385504505..950dc8745b3 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 e0f66bc210d..6714d6986b2 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 ea6b2e36696..deb6d926511 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 d4a291e1ca5..c1748032905 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 8c84df60c45..4c37d351ce4 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 276603c4eaf..cda82de061d 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 2ebbb6c4b18..ef09af89e6d 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 55ffe2c2f62..395c1000004 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
--
GitLab