diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 4b15b9a2a61e705e32caf006307f3a0d50a4bb88..a401f52df2d32e92c9d92629b4c134a7ea710e91 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -260,7 +260,7 @@ module Alarm_cache =
State_builder.Hashtbl (Alarm_key.Hashtbl) (Datatype.Unit)
(struct
let name = "Value_messages.Alarm_cache"
- let dependencies = [Db.Value.self]
+ let dependencies = [Self.state]
let size = 35
end)
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 57c2a2a984850adb88d2986352600e6432fca833..ca1f01b8dfe1720690a23cf30ee7be3336f656cc 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -50,7 +50,7 @@ let builtins_table = Hashtbl.create 17
module Info = struct
let name = "Eva.Builtins.BuiltinsOverride"
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Self.state ]
end
(** Set of functions overridden by a builtin. *)
module BuiltinsOverride = State_builder.Set_ref (Kernel_function.Set) (Info)
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index f2d0655ff0227c5ba270ea489adb689a0fa3718e..30f759714e8cfc17ba224a5d46b96a26c68e2ddf 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -451,7 +451,7 @@ module State = struct
module Storage =
State_builder.Ref (Datatype.Bool)
(struct
- let dependencies = [Db.Value.self]
+ let dependencies = [Self.state]
let name = name ^ ".Storage"
let default () = false
end)
diff --git a/src/plugins/value/domains/domain_store.ml b/src/plugins/value/domains/domain_store.ml
index 716bb29bb57404a8f56baf0ed268f1e1684ff6d9..4bfa88ec212360792cd1fc8eba6764be6d32585b 100644
--- a/src/plugins/value/domains/domain_store.ml
+++ b/src/plugins/value/domains/domain_store.ml
@@ -58,9 +58,9 @@ module Make (Domain: InputDomain) = struct
(* This module stores the resulting states of an Eva analysis. They depends on
the set of parameters with which the analysis has been run, and must be
cleared each time one of this parameter is changed. Thus, the tables of
- this module have as dependencies Db.Value.self, the internal state of Eva
+ this module have as dependencies Self.state, the internal state of Eva
(all parameters of Eva are added as codependencies of this state). *)
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Self.state ]
let size = 16
module type Ref = sig
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 4542b3f71043fe7379d47cfc53e545bfe0a861d8..122e2c5ca6c2656f4da3339c1b80fc101dfcae1c 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -134,7 +134,7 @@ struct
let name = "Eva.Analysis.ComputationState"
let pretty fmt s = Format.pp_print_string fmt (to_string s)
let reprs = [ NotComputed ; Computing ; Computed ]
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Self.state ]
let default () = NotComputed
end
@@ -224,7 +224,7 @@ let is_computed = Db.Value.is_computed
let compute () =
(* Nothing to recompute when Value has already been computed. This boolean
is automatically cleared when an option of Value changes, because they
- are registered as dependencies on [Db.Value.self] in {!Parameters}.*)
+ are registered as dependencies on [Self.state] in {!Parameters}.*)
if not (is_computed ()) then force_compute ()
(* Resets the Analyzer when the current project is changed. *)
@@ -233,4 +233,4 @@ let () =
~user_only:true (fun _ -> reset_analyzer ());
Project.register_after_global_load_hook reset_analyzer
-let self = Db.Value.self
+let self = Self.state
diff --git a/src/plugins/value/engine/initialization.ml b/src/plugins/value/engine/initialization.ml
index 9e50efb58ac81dbc351c8491d9a61971ec053900..34df9813bc398fda5ec1fdd1c7a784a1436b1402 100644
--- a/src/plugins/value/engine/initialization.ml
+++ b/src/plugins/value/engine/initialization.ml
@@ -327,7 +327,7 @@ module Make
(* Dependencies for the Frama-C states containing the initial states
of Eva: all correctness parameters of Eva, plus the AST itself. We
- cannot use [Db.Value.self] directly, because we do not want to
+ cannot use [Self.state] directly, because we do not want to
depend on the tuning parameters. Previously, we use a more
fine-grained list, but this lead to bugs. See mantis #2277. *)
let correctness_deps =
diff --git a/src/plugins/value/engine/mem_exec.ml b/src/plugins/value/engine/mem_exec.ml
index 54c5d3f5e9fed0290d05a783a031fb9d0db34f70..35dc3f3e2af0a27abdcc234ced3e5731cda64369 100644
--- a/src/plugins/value/engine/mem_exec.ml
+++ b/src/plugins/value/engine/mem_exec.ml
@@ -82,7 +82,7 @@ module Make
(ArgsToStoredCalls)
(struct
let size = 17
- let dependencies = [Db.Value.self]
+ let dependencies = [Self.state]
let name = "Mem_exec.PreviousCalls(" ^ string_of_int !counter ^ ")"
end)
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 47358794f67e3e190617d78e9ede7d24087e9dd2..3fe6dfc5177afc92d221a8f87bf8d492743fb98e 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -51,7 +51,7 @@ end
module InOutCallback =
State_builder.Option_ref (Inout_type)
(struct
- let dependencies = [Db.Value.self]
+ let dependencies = [Self.state]
let name = "Transfer_stmt.InOutCallback"
end)
@@ -99,7 +99,7 @@ module DumpFileCounters =
State_builder.Hashtbl (Datatype.String.Hashtbl) (Datatype.Int)
(struct
let size = 3
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Self.state ]
let name = "Transfer_stmt.DumpFileCounters"
end)
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 2b2cb3425ba21500297751bc07361f91c0f7b8ee..ab3a7c10f477e391ad59ac9994716189d6862bd3 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -35,7 +35,7 @@ module UsedVarState =
(struct
let size = 17
let name = "Value.Gui.UsedVarState"
- let dependencies = [ Analysis.self ]
+ let dependencies = [ Self.state ]
(* [!Db.Inputs.self_external; !Db.Outputs.self_external] would be better
dependencies, but this introduces a very problematic recursion between
Value and Inout *)
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index 8bf1ae4ac30d4fcb06cce1f7a649a7663e6b84a0..625c90273b3155bb2b5f86e38a33a260ee9797c8 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -24,10 +24,10 @@ open Cil_types
open Locations
let [@alert "-deprecated"] _self =
- Db.register_compute "Value.compute" [ Db.Value.self ] Db.Value.compute
+ Db.register_compute "Value.compute" [ Self.state ] Db.Value.compute
Analysis.compute
-let () = Parameters.ForceValues.set_output_dependencies [Db.Value.self]
+let () = Parameters.ForceValues.set_output_dependencies [Self.state]
let main () =
(* Value computations *)
diff --git a/src/plugins/value/utils/eva_results.ml b/src/plugins/value/utils/eva_results.ml
index bab62ba7d48b4ffb1f96b39223e7a617d0d90117..2762f635332dddd73d8003e2524baa4ac3af890a 100644
--- a/src/plugins/value/utils/eva_results.ml
+++ b/src/plugins/value/utils/eva_results.ml
@@ -29,7 +29,7 @@ module Is_Called =
(Datatype.Bool)
(struct
let name = "Value.Eva_results.is_called"
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Self.state ]
let size = 17
end)
@@ -50,7 +50,7 @@ module Callers =
(Kernel_function.Map.Make(Stmt.Set))
(struct
let name = "Value.Eva_results.Callers"
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Self.state ]
let size = 17
end)
@@ -202,9 +202,9 @@ let get_results () =
initial_state; initial_args; alarms; statuses; main }
let set_results results =
- let selection = State_selection.with_dependencies Db.Value.self in
+ let selection = State_selection.with_dependencies Self.state in
Project.clear ~selection ();
- (* Those two functions may clear Db.Value.self. Start by them *)
+ (* Those two functions may clear Self.state. Start by them *)
(* Initial state *)
Db.Value.globals_set_initial_state results.initial_state;
(* Initial args *)
diff --git a/src/plugins/value/utils/eva_utils.ml b/src/plugins/value/utils/eva_utils.ml
index 5f0438cc7808d0da495efcff1220fb40ff3c7769..6220ca09e8006d925766a9c3063e6225cfad899a 100644
--- a/src/plugins/value/utils/eva_utils.ml
+++ b/src/plugins/value/utils/eva_utils.ml
@@ -104,7 +104,7 @@ module DegenerationPoints =
(struct
let name = "Eva_utils.Degeneration"
let size = 17
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Self.state ]
end)
let protect_only_once = ref true
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index c9b81edc45245610137f78afe256624bd9b5e691..5aa2f284c1193e2ed95822df94a8d563e512bfb4 100644
--- a/src/plugins/value/utils/library_functions.ml
+++ b/src/plugins/value/utils/library_functions.ml
@@ -33,7 +33,7 @@ module Retres =
let () = Ast.add_monotonic_state Retres.self
let () =
- State_dependency_graph.add_dependencies ~from:Retres.self [ Db.Value.self ]
+ State_dependency_graph.add_dependencies ~from:Retres.self [ Self.state ]
let get_retres_vi = Retres.memo
(fun kf ->
diff --git a/src/plugins/value/utils/red_statuses.ml b/src/plugins/value/utils/red_statuses.ml
index 903319a436be509cb32fcace07f57c78b6e9b324..c7e0ca34d290064375bae71bac59c7b2fed8f759 100644
--- a/src/plugins/value/utils/red_statuses.ml
+++ b/src/plugins/value/utils/red_statuses.ml
@@ -64,7 +64,7 @@ module RedStatusesTable =
(struct
let name = "Value.Red_statuses.RedStatusesTable"
let size = 16
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Self.state ]
end)
let add_red_ap kinstr ap =
diff --git a/src/plugins/value/utils/summary.ml b/src/plugins/value/utils/summary.ml
index 2ed7573fe071ad06ebb97d39ae6cdf641cc0ecf8..c75d03fb740c4d8e94f3de402dc78950783c6288 100644
--- a/src/plugins/value/utils/summary.ml
+++ b/src/plugins/value/utils/summary.ml
@@ -207,7 +207,7 @@ module FunctionStats = struct
(FunctionStats_Type)
(struct
let name = "Eva.Summary.FunctionStats"
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Self.state ]
let size = 17
end)
diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index 05a9e0477af7e53e752b2c68e778a4d5b53bf4d4..c22541b345139366301de50bf2d6de2c037e0950 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/src/plugins/value/utils/widen.ml
@@ -493,7 +493,7 @@ module Parsed_Dynamic_Hints =
(struct
let name = "Widen.Parsed_Dynamic_Hints"
let size = 7
- let dependencies = [ Ast.self; Db.Value.self ]
+ let dependencies = [ Ast.self; Self.state ]
end)
let dynamic_bases_of_lval states e offset =
@@ -530,7 +530,7 @@ module Dynamic_Hints =
State_builder.Ref
(Widen_type)
(struct
- let dependencies = [ Ast.self; Db.Value.self ]
+ let dependencies = [ Ast.self; Self.state ]
let name = "Widen.Dynamic_Hints"
let default = Widen_type.default
end)