diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index b63abe98dc97998803b7e77f354a53aebedc043d..950e5d6150e13b42abbec2f706b23014a59104b7 100644 --- a/src/kernel_services/plugin_entry_points/db.ml +++ b/src/kernel_services/plugin_entry_points/db.ml @@ -266,14 +266,10 @@ module Value = struct let globals_use_supplied_state () = not (VGlobals.get_option () = None) - (* Do NOT add dependencies to Kernel parameters here, but at the top of - Value/Value_parameters *) - let dependencies = - [ Ast.self; - Alarms.self; - Annotations.code_annot_state; - FunArgs.self; - VGlobals.self ] + let dependencies = [ FunArgs.self; VGlobals.self ] + let proxy = State_builder.Proxy.(create "eva_db" Forward dependencies) + let self = State_builder.Proxy.get proxy + let only_self = [ self ] let size = 256 @@ -285,14 +281,14 @@ module Value = struct (struct let name = "Db.Value.Table_By_Callstack" let size = size - let dependencies = dependencies + let dependencies = [ self ] end) module Table = Cil_state_builder.Stmt_hashtbl(Cvalue.Model) (struct let name = "Db.Value.Table" let size = size - let dependencies = [ Table_By_Callstack.self ] + let dependencies = [ self ] end) (* Clear Value's various caches each time [Db.Value.is_computed] is updated, including when it is set, reset, or during project change. Some operations @@ -308,26 +304,21 @@ module Value = struct Function_Froms.Memory.clear_caches (); ) - module AfterTable_By_Callstack = Cil_state_builder.Stmt_hashtbl(States_by_callstack) (struct let name = "Db.Value.AfterTable_By_Callstack" let size = size - let dependencies = [ Table_By_Callstack.self ] + let dependencies = [ self ] end) module AfterTable = Cil_state_builder.Stmt_hashtbl(Cvalue.Model) (struct let name = "Db.Value.AfterTable" let size = size - let dependencies = [ AfterTable_By_Callstack.self ] + let dependencies = [ self ] end) - - let self = Table_By_Callstack.self - let only_self = [ self ] - let mark_as_computed = Journal.register "Db.Value.mark_as_computed" (Datatype.func Datatype.unit Datatype.unit) diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index 636ec1d8bd5a8f8b59f10256faf861772fc4edd7..d944d48b1542b56f9ba69055785a45640203ab1a 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -129,6 +129,8 @@ module Value : sig val emitter: Emitter.t ref (** Emitter used by Value to emit statuses *) + val proxy: State_builder.Proxy.t + val self : State.t (** Internal state of the value analysis from projects viewpoint. @plugin development guide *) diff --git a/src/plugins/value/parameters.ml b/src/plugins/value/parameters.ml index 0b994b78bd745a3db7b42fabc53a6404cbaa39ea..c03116c950d4c2eaba727f456f89bc2facc512be 100644 --- a/src/plugins/value/parameters.ml +++ b/src/plugins/value/parameters.ml @@ -45,9 +45,8 @@ let kernel_parameters_correctness = [ let parameters_correctness = ref Typed_parameter.Set.empty let parameters_tuning = ref Typed_parameter.Set.empty let add_dep p = - State_dependency_graph.add_codependencies - ~onto:Db.Value.self - [State.get p.Typed_parameter.name] + let state = State.get p.Typed_parameter.name in + State_builder.Proxy.extend [state] Self.proxy let add_correctness_dep p = if Typed_parameter.Set.mem p !parameters_correctness then Kernel.abort "adding correctness parameter %a twice" diff --git a/src/plugins/value/self.ml b/src/plugins/value/self.ml index 69af425301a4a9e69349acf600b3ce8788f8a8bb..660ac61d9a5f179f2174c4e36ef8592439c07101 100644 --- a/src/plugins/value/self.ml +++ b/src/plugins/value/self.ml @@ -28,6 +28,20 @@ include Plugin.Register "automatically computes variation domains for the variables of the program" end) +(* Do not add dependencies to Kernel parameters here, but at the top of + Parameters. *) +let kernel_dependencies = + [ Ast.self; + Alarms.self; + Annotations.code_annot_state; ] + +let dependencies = Db.Value.self :: kernel_dependencies + +let proxy = State_builder.Proxy.(create "eva" Forward dependencies) +let state = State_builder.Proxy.get proxy + +let () = State_builder.Proxy.extend [state] Db.Value.proxy + let () = Help.add_aliases ~visible:false [ "-value-h"; "-val-h" ] let () = add_plugin_output_aliases ~visible:false ~deprecated:true [ "value" ] diff --git a/src/plugins/value/self.mli b/src/plugins/value/self.mli index 94cd9910a275e60fd0c2b491c18bd430399f69d3..cd4de22ea767957d005d1cba9f703b5ed73eb4ab 100644 --- a/src/plugins/value/self.mli +++ b/src/plugins/value/self.mli @@ -22,6 +22,9 @@ include Plugin.General_services +val proxy: State_builder.Proxy.t +val state: State.t + (** Debug categories responsible for printing initial and final states of Value. Enabled by default, but can be disabled via the command-line: -value-msg-key="-initial_state,-final_state" *)