[Eva] API: exports the analysis_status of any function.

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

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

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

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