From 7db9febde9b931c81d7628269db1a3659aff8860 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 3 Aug 2023 12:35:56 +0200
Subject: [PATCH] [Eva] Finally removes deprecated module Db.Value.
---
src/kernel_services/plugin_entry_points/db.ml | 17 ----------
.../plugin_entry_points/db.mli | 32 -------------------
src/plugins/eva/Eva.mli | 1 -
src/plugins/eva/dune | 4 +--
src/plugins/eva/engine/analysis.ml | 1 -
src/plugins/eva/legacy/TOREMOVE | 5 ---
src/plugins/eva/self.ml | 7 +---
src/plugins/eva/types/callstack.mli | 1 -
8 files changed, 3 insertions(+), 65 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 3f7b06b545f..69383faea0b 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 037888db0e7..ff51d3e0f5b 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 c8c32af8d90..33d434deb98 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 9a3d06be432..7023a1e2086 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 06aa0bce44b..aee5de68bf0 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 a45847d25ad..7fc89bce7fe 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 072213e1a68..e802fe89a78 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 76701e429dc..f63751e19d9 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
--
GitLab