diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index 2e3d4229914d91019e197563e43235ce6b6462ad..2ba86cfddf58dda836d6fce0e768bfa3d7fe71e9 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/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 diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune index 771f0d370a7ef9ea85f2b87dc2a5c606d4f71418..5a4d1269347687f00cf1c53ff96fbea4929c3540 100644 --- a/src/plugins/eva/dune +++ b/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 diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml index cab823fbddcd551f41fab6cf076920875f52eb13..65ad9b3a4f1274c55653b2665b09b5f5e090af97 100644 --- a/src/plugins/scope/datascope.ml +++ b/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