[Eva] API: exports [no_results].

src/plugins/value/engine/analysis.ml

@@ -29,6 +29,10 @@ let current_computation_state = Self.current_computation_state
 let register_computation_hook = Self.register_computation_hook
 let is_computed = Self.is_computed
 
+let save_results kf =
+  try Function_calls.save_results (Kernel_function.get_definition kf)
+  with Kernel_function.No_Definition -> false
+
 module type Results = sig
   type state
   type value

src/plugins/value/engine/analysis.mli

@@ -144,6 +144,11 @@ val status: Cil_types.kernel_function -> status
     Please use {!Eva.Results.are_available} instead to known whether results
     are available for a given function. *)
 val use_spec_instead_of_definition: Cil_types.kernel_function -> bool
+
+(** Returns [true] if the user has requested that no results should be recorded
+    for the given function. Please use {!Eva.Results.are_available} instead
+    to known whether results are available for a given function. *)
+val save_results: Cil_types.kernel_function -> bool
 [@@@ api_end]
 
 val cvalue_initial_state: unit -> Cvalue.Model.t

src/plugins/value/engine/function_calls.mli

@@ -22,6 +22,9 @@
 
 open Cil_types
 
+(** True if the results should be saved for the given function. *)
+val save_results: fundec -> bool
+
 (** What is used for the analysis of a given function:
     - a Cvalue builtin (and other domains use the specification)
     - the function specification