[Eva] New Frama-C state Self.state to replace Db.Value.self.

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)

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 *)

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"

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" ]
 

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" *)