diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 3f7b06b545ff683e9835a9654c8312cc36222e5f..69383faea0bdae2dd7329a0d55062024fac86df0 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -157,23 +157,6 @@ module Derefs = struct
let pretty = Locations.Zone.pretty
end
-
-(* ************************************************************************* *)
-(** {2 Values} *)
-(* ************************************************************************* *)
-
-module Value = struct
- type state = Cvalue.Model.t
- type t = Cvalue.V.t
-
- let dependencies = [ ]
- let proxy = State_builder.Proxy.(create "eva_db" Forward dependencies)
- let self = State_builder.Proxy.get proxy
-
- let compute = mk_fun "Value.compute"
-
-end
-
(* ************************************************************************* *)
(** {2 Others plugins} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 037888db0e7338f80b980eee05ce439b9b8efa9c..ff51d3e0f5b15023c5b7e1fd665756a7f5c85313 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -96,38 +96,6 @@ module Toplevel: sig
end
-(* ************************************************************************* *)
-(** {2 Values} *)
-(* ************************************************************************* *)
-
-(** Deprecated module: use the Eva.mli API instead. *)
-module Value : sig
-
- type state = Cvalue.Model.t
- (** Internal state of the value analysis. *)
-
- type t = Cvalue.V.t
- (** Internal representation of a value. *)
-
- val proxy: State_builder.Proxy.t
-
- val self : State.t
- (** Internal state of the value analysis from projects viewpoint.
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-
- val compute : (unit -> unit) ref
- (** Compute the value analysis using the entry point of the current
- project. You may set it with {!Globals.set_entry_point}.
- @raise Globals.No_such_entry_point if the entry point is incorrect
- @raise Db.Value.Incorrect_number_of_arguments if some arguments are
- specified for the entry point using {!Db.Value.fun_set_args}, and
- an incorrect number of them is given.
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-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."]
-
(* ************************************************************************* *)
(** {2 Plugins} *)
(* ************************************************************************* *)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index c8c32af8d90dba5a9c34499454eb96b0caba795f..33d434deb9819cfe16e8506fe206fc62e690cf59 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -113,7 +113,6 @@ module Analysis: sig
end
module Callstack: sig
- [@@@ alert "-db_deprecated"]
(** A call is identified by the function called and the call statement *)
type call = Cil_types.kernel_function * Cil_types.stmt
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 9a3d06be43283a6417be2fcede82b8b3c1b54090..7023a1e20869441630a0ce257e11798603971a3f 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -40,7 +40,7 @@
(name eva)
(optional)
(public_name frama-c-eva.core)
- (flags -open Frama_c_kernel :standard -w -9 -alert -db_deprecated)
+ (flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-server.core)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
@@ -60,7 +60,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 -alert -db_deprecated)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9)
(libraries eva frama-c.kernel frama-c.gui)
(instrumentation (backend landmarks))))
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index 06aa0bce44b1c7290400f61d59edf71f381e680d..aee5de68bf0f43530d7fad97ae8be115ad7c227a 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -229,7 +229,6 @@ let compute =
let name = "Eva.Analysis.compute" in
fst (State_builder.apply_once name [ Self.state ] compute)
-let () = Db.Value.compute := compute
let () = Parameters.ForceValues.set_output_dependencies [Self.state]
let main () =
diff --git a/src/plugins/eva/legacy/TOREMOVE b/src/plugins/eva/legacy/TOREMOVE
index a45847d25ad5d534973f2563e1c31130ecacab8f..7fc89bce7fe16e277a92ae32d0c20bcce97b3df6 100644
--- a/src/plugins/eva/legacy/TOREMOVE
+++ b/src/plugins/eva/legacy/TOREMOVE
@@ -1,11 +1,6 @@
-**Function_args**: only there to fill Db.Value.add_formals_to_state, itself used
- by Inout/Cumulative_analysis. [compute_actual] is now in [Transfer_stmt],
- [actualize_formals] is in [Cvalue_transfer]
-
**Eval_op**: multiple dependencies in Eval_terms and builtins. Must be rewritten
into the corresponding functionality in Cvalue_forward. This requires having
contexts for logic terms, though.
-
To be moved elsewhere, probably in domains/cvalue or in engine:
eval_annots, eval_terms
diff --git a/src/plugins/eva/self.ml b/src/plugins/eva/self.ml
index 072213e1a68c550fc1389bb697e0d79b71937b1c..e802fe89a788a0f252b63391adc6d03ae6dea5a0 100644
--- a/src/plugins/eva/self.ml
+++ b/src/plugins/eva/self.ml
@@ -38,14 +38,9 @@ let kernel_dependencies =
Alarms.self;
Annotations.code_annot_state; ]
-let dependencies = Db.Value.self :: kernel_dependencies
-
-let proxy = State_builder.Proxy.(create "eva" Forward dependencies)
+let proxy = State_builder.Proxy.(create "eva" Forward kernel_dependencies)
let state = State_builder.Proxy.get proxy
-let () = State_builder.Proxy.extend [state] Db.Value.proxy
-
-
(* Current state of the analysis *)
type computation_state = NotComputed | Computing | Computed | Aborted
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 76701e429dcc298daca823dc8673760ef03d4417..f63751e19d9ecf65bea5d2f19db6ee7474200be2 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -21,7 +21,6 @@
(**************************************************************************)
[@@@ api_start]
-[@@@ alert "-db_deprecated"]
(** A call is identified by the function called and the call statement *)
type call = Cil_types.kernel_function * Cil_types.stmt