From c700164e319959561ac26da163a06192ccd401bc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 22 Feb 2022 09:42:02 +0100
Subject: [PATCH] [Eva] API: exports the analysis_status of any function.
---
src/plugins/value/engine/analysis.ml | 5 ++++
src/plugins/value/engine/analysis.mli | 32 +++++++++++++++++++++
src/plugins/value/engine/function_calls.ml | 4 +++
src/plugins/value/engine/function_calls.mli | 10 ++++++-
4 files changed, 50 insertions(+), 1 deletion(-)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index ca477158425..f8adbfbb0d2 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -203,3 +203,8 @@ let () =
Project.register_after_global_load_hook reset_analyzer
let self = Self.state
+
+type results = Function_calls.results = Complete | Partial | NoResults
+type status = Function_calls.analysis_status =
+ Unreachable | SpecUsed | Builtin of string | Analyzed of results
+let status = Function_calls.analysis_status
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index 510972db918..e74658ef216 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -106,6 +106,38 @@ val is_computed : unit -> bool
val self : State.t
(** Internal state of Eva analysis from projects viewpoint. *)
+
+(** Kind of results for the analysis of a function body. *)
+type results =
+ | Complete
+ (** The results are complete: they cover all possible call contexts of the
+ given function. *)
+ | Partial
+ (** The results are partial, as the functions has not been analyzed in all
+ possible call contexts. This happens for recursive functions that are
+ not completely unrolled, or if the analysis has stopped unexpectedly. *)
+ | NoResults
+ (** No results were saved for the function, due to option -eva-no-results.
+ Any request at a statement of this function will lead to a Top result. *)
+
+(* Analysis status of a function. *)
+type status =
+ | Unreachable
+ (** The function has not been reached by the analysis. Any request in thi
+ function will lead to a Bottom result. *)
+ | SpecUsed
+ (** The function specification has been used to interpret its calls:
+ its body has not been analyzed. Any request at a statement of this
+ function will lead to a Top result. *)
+ | Builtin of string
+ (** The builtin of the given name has been used to interpret the function:
+ its body has not been analyzed. Any request at a statement of this
+ function will lead to a Top result. *)
+ | Analyzed of results
+ (** The function body has been analyzed. *)
+
+(** Returns the analysis status of a given function. *)
+val status: Cil_types.kernel_function -> status
[@@@ api_end]
val cvalue_initial_state: unit -> Cvalue.Model.t
diff --git a/src/plugins/value/engine/function_calls.ml b/src/plugins/value/engine/function_calls.ml
index afefe850a77..eff7dbc77a5 100644
--- a/src/plugins/value/engine/function_calls.ml
+++ b/src/plugins/value/engine/function_calls.ml
@@ -118,6 +118,10 @@ let register_status kf kind =
in
ignore (StatusTable.memo ~change (fun _ -> status) kf)
+let analysis_status kf =
+ try StatusTable.find kf
+ with Not_found -> Unreachable
+
let analysis_target ~recursion_depth callsite kf =
match Builtins.find_builtin_override kf with
diff --git a/src/plugins/value/engine/function_calls.mli b/src/plugins/value/engine/function_calls.mli
index 49bd5a338f7..3dbf96314e3 100644
--- a/src/plugins/value/engine/function_calls.mli
+++ b/src/plugins/value/engine/function_calls.mli
@@ -35,7 +35,7 @@ type analysis_target =
(** Define the analysis target of a function according to Eva parameters.
Also registers the call in tables for the functions below. *)
val define_analysis_target:
- ?recursion_depth:int -> kinstr -> kernel_function -> analysis_target
+ ?recursion_depth:int -> kinstr -> kernel_function -> analysis_target
(** Returns true if the function has been analyzed. *)
@@ -47,3 +47,11 @@ val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
(** Returns the list of inferred callers, and for each of them, the list
of callsites (the call statements) inside. *)
val callsites: kernel_function -> (kernel_function * stmt list) list
+
+
+type results = Complete | Partial | NoResults
+type analysis_status =
+ Unreachable | SpecUsed | Builtin of string | Analyzed of results
+
+(** Returns the current analysis status of a given function. *)
+val analysis_status: kernel_function -> analysis_status
--
GitLab