diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml index 17575ba0ac363c88861db0607aa8558c55201977..9b43b96fa2f12d3164b21b7c8e7a80b10182d0a8 100644 --- a/src/plugins/value/engine/analysis.ml +++ b/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 diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli index 8d06f8667a024d2fbe3b30b9e911414289e82a32..98c2201b905cd1ea8911de7f2448766be0f3d384 100644 --- a/src/plugins/value/engine/analysis.mli +++ b/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 diff --git a/src/plugins/value/engine/function_calls.mli b/src/plugins/value/engine/function_calls.mli index 3dbf96314e3ff250d32f05e3d28c4ff998bc666d..698b62406e5db83c76b697e55acfe2d9f5169b62 100644 --- a/src/plugins/value/engine/function_calls.mli +++ b/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