From e922e0f7804700f8d23590bc5dd583999dd28400 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 19 Jul 2022 15:03:57 +0200
Subject: [PATCH] [Eva] Deprecates Db.Value.
---
src/kernel_services/plugin_entry_points/db.mli | 14 ++++++++------
src/plugins/eva/dune | 4 ++--
src/plugins/scope/datascope.ml | 3 +--
3 files changed, 11 insertions(+), 10 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 2e3d4229914..2ba86cfddf5 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 771f0d370a7..5a4d1269347 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 cab823fbddc..65ad9b3a4f1 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
--
GitLab