[Eva] Results: exports [are_available].

src/plugins/value/utils/results.ml

@@ -22,6 +22,11 @@
 
 open Lattice_bounds
 
+let are_available kf =
+  match Analysis.status kf with
+  | Analyzed (Complete | Partial) -> true
+  | SpecUsed | Builtin _ | Unreachable | Analyzed NoResults -> false
+
 module Callstack = Value_types.Callstack
 
 type callstack = Callstack.t

src/plugins/value/utils/results.mli

@@ -54,6 +54,16 @@
       default O (as_int (eval_var vi (in_callstack cs (before stmt))))
 *)
 
+(** Are results available for a given function? True if the function body has
+    been has been analyzed and the results have been saved.
+    False if:
+    - the function has not been reached by the analysis: all requests in the
+      function will lead to a Bottom error.
+    - a specification or a builtin has been used instead of analyzing the
+      function body: all requests in the function will lead to a Top error.
+    - results have not been saved, due to the [-eva-no-results] parameter:
+      all requests in the function will lead to a Top error. *)
+val are_available: Cil_types.kernel_function -> bool
 
 type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list