From f6c1cd1475c681029d1523e858f758fef2696615 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 17 Jan 2022 22:25:47 +0100
Subject: [PATCH] [Eva] Replaces Db.Value.self by Self.state.
---
src/plugins/value/alarmset.ml | 2 +-
src/plugins/value/domains/cvalue/builtins.ml | 2 +-
src/plugins/value/domains/cvalue/cvalue_domain.ml | 2 +-
src/plugins/value/domains/domain_store.ml | 4 ++--
src/plugins/value/engine/analysis.ml | 6 +++---
src/plugins/value/engine/initialization.ml | 2 +-
src/plugins/value/engine/mem_exec.ml | 2 +-
src/plugins/value/engine/transfer_stmt.ml | 4 ++--
src/plugins/value/gui_files/register_gui.ml | 2 +-
src/plugins/value/register.ml | 4 ++--
src/plugins/value/utils/eva_results.ml | 8 ++++----
src/plugins/value/utils/eva_utils.ml | 2 +-
src/plugins/value/utils/library_functions.ml | 2 +-
src/plugins/value/utils/red_statuses.ml | 2 +-
src/plugins/value/utils/summary.ml | 2 +-
src/plugins/value/utils/widen.ml | 4 ++--
16 files changed, 25 insertions(+), 25 deletions(-)
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 4b15b9a2a61..a401f52df2d 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 57c2a2a9848..ca1f01b8dfe 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 f2d0655ff02..30f759714e8 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 716bb29bb57..4bfa88ec212 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 4542b3f7104..122e2c5ca6c 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 9e50efb58ac..34df9813bc3 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 54c5d3f5e9f..35dc3f3e2af 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 47358794f67..3fe6dfc5177 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 2b2cb3425ba..ab3a7c10f47 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 8bf1ae4ac30..625c90273b3 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 bab62ba7d48..2762f635332 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 5f0438cc780..6220ca09e80 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 c9b81edc452..5aa2f284c11 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 903319a436b..c7e0ca34d29 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 2ed7573fe07..c75d03fb740 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 05a9e0477af..c22541b3451 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)
--
GitLab