From f48ddd6c3235fa4a9143f2388fb8c530b926ea6e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 21 Jul 2022 09:57:02 +0200
Subject: [PATCH] [Eva] Documents the part of the Eva API that are for internal
use only.
---
src/plugins/eva/Eva.mli | 14 +++++++++++---
src/plugins/eva/utils/cvalue_callbacks.mli | 5 ++++-
src/plugins/eva/utils/eva_results.mli | 4 ++++
src/plugins/eva/utils/results.mli | 5 +++--
4 files changed, 22 insertions(+), 6 deletions(-)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 9f0d113f787..5fc9ded3be8 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -212,8 +212,9 @@ module Results: sig
(** Just before a statement or at the start of the analysis. *)
val before_kinstr : Cil_types.kinstr -> request
- (** Evaluation in a given cvalue state.
- Callstacks selection are silently ignored on such requests. *)
+ (** Evaluation in a given cvalue state. Callstacks selection are silently
+ ignored on such requests. For internal use, could be modified or removed
+ in a future version. *)
val in_cvalue_state : Cvalue.Model.t -> request
@@ -594,7 +595,10 @@ end
module Cvalue_callbacks: sig
(** Register actions to performed during the Eva analysis,
- with access to the states of the cvalue domain. *)
+ with access to the states of the cvalue domain.
+ This API is for internal use only, and may be modified or removed
+ in a future version. Please contact us if you need to register callbacks
+ to be executed during an Eva analysis. *)
type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
type state = Cvalue.Model.t
@@ -674,6 +678,10 @@ module Logic_inout: sig
end
module Eva_results: sig
+
+ (** Internal temporary API: please do not use it, as it should be removed in a
+ future version. *)
+
type results
val get_results: unit -> results
diff --git a/src/plugins/eva/utils/cvalue_callbacks.mli b/src/plugins/eva/utils/cvalue_callbacks.mli
index cb26f37aa10..3122b1b3c65 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.mli
+++ b/src/plugins/eva/utils/cvalue_callbacks.mli
@@ -23,7 +23,10 @@
[@@@ api_start]
(** Register actions to performed during the Eva analysis,
- with access to the states of the cvalue domain. *)
+ with access to the states of the cvalue domain.
+ This API is for internal use only, and may be modified or removed
+ in a future version. Please contact us if you need to register callbacks
+ to be executed during an Eva analysis. *)
type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
type state = Cvalue.Model.t
diff --git a/src/plugins/eva/utils/eva_results.mli b/src/plugins/eva/utils/eva_results.mli
index 6144615c2e4..19e35f6bd7b 100644
--- a/src/plugins/eva/utils/eva_results.mli
+++ b/src/plugins/eva/utils/eva_results.mli
@@ -30,6 +30,10 @@ val is_non_terminating_instr: stmt -> bool
(** {2 Results} *)
[@@@ api_start]
+
+(** Internal temporary API: please do not use it, as it should be removed in a
+ future version. *)
+
type results
val get_results: unit -> results
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index 30806c77475..ec7bc51d785 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -117,8 +117,9 @@ val after : Cil_types.stmt -> request
(** Just before a statement or at the start of the analysis. *)
val before_kinstr : Cil_types.kinstr -> request
-(** Evaluation in a given cvalue state.
- Callstacks selection are silently ignored on such requests. *)
+(** Evaluation in a given cvalue state. Callstacks selection are silently
+ ignored on such requests. For internal use, could be modified or removed
+ in a future version. *)
val in_cvalue_state : Cvalue.Model.t -> request
--
GitLab