[Eva] Deprecates Db.Value.

src/kernel_services/plugin_entry_points/db.mli

@@ -100,8 +100,7 @@ end
 (** {2 Values} *)
 (* ************************************************************************* *)
 
-(** The Value analysis itself.
-    @see <../value/index.html> internal documentation. *)
+(** Deprecated module: use the Eva.mli API instead. *)
 module Value : sig
 
   type state = Cvalue.Model.t
@@ -500,6 +499,9 @@ module Value : sig
 
   val initial_state_changed: (unit -> unit) ref
 end
+[@@alert db_deprecated
+    "Db.Value is deprecated and will be removed in a future version \
+     of Frama-C. Please use the Eva.mli public API instead."]
 
 (** Functional dependencies between function inputs and function outputs.
     @see <../from/index.html> internal documentation. *)
@@ -528,11 +530,11 @@ module From : sig
   val find_deps_no_transitivity : (stmt -> exp -> Locations.Zone.t) ref
 
   val find_deps_no_transitivity_state :
-    (Value.state -> exp -> Locations.Zone.t) ref
+    (Cvalue.Model.t -> exp -> Locations.Zone.t) ref
 
   (** @raise Not_lval if the given expression is not a C lvalue. *)
   val find_deps_term_no_transitivity_state :
-    (Value.state -> term -> Value_types.logic_dependencies) ref
+    (Cvalue.Model.t -> term -> Value_types.logic_dependencies) ref
 
   val self: State.t ref
 
@@ -637,12 +639,12 @@ module Properties : sig
     (** {3 From logic terms to Locations.location} *)
 
     val loc_to_loc:
-      (result: Cil_types.varinfo option -> Value.state -> term ->
+      (result: Cil_types.varinfo option -> Cvalue.Model.t -> term ->
        Locations.location) ref
     (** @raise No_conversion if the translation fails. *)
 
     val loc_to_loc_under_over:
-      (result: Cil_types.varinfo option -> Value.state -> term ->
+      (result: Cil_types.varinfo option -> Cvalue.Model.t -> term ->
        Locations.location * Locations.location * Locations.Zone.t) ref
     (** Same as {!loc_to_loc}, except that we return simultaneously an
         under-approximation of the term (first location), and an

src/plugins/eva/dune

@@ -38,7 +38,7 @@
  (name eva)
  (optional)
  (public_name frama-c-eva.core)
- (flags -open Frama_c_kernel :standard -w -9)
+ (flags -open Frama_c_kernel :standard -w -9 -alert -db_deprecated)
  (libraries frama-c.kernel frama-c-server.core))
 
 (plugin
@@ -55,7 +55,7 @@
   (name eva_gui)
   (optional)
   (public_name frama-c-eva.gui)
-  (flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9)
+  (flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9 -alert -db_deprecated)
   (libraries eva frama-c.kernel frama-c.gui)))
 
 (plugin

src/plugins/scope/datascope.ml

@@ -640,8 +640,7 @@ let rm_asserts () =
   end
 
 
-let () =
-  Db.register   Db.Value.rm_asserts rm_asserts
+let () = Db.register Db.Value.rm_asserts rm_asserts [@alert "-db_deprecated"]
 
 let rm_asserts =
   Dynamic.register