From 7a5ec248f6cb71a9ac07ad0e8bbc1a97b304ae40 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 16 Mar 2022 15:00:49 +0100
Subject: [PATCH] [Eva] API: exports [no_results].
---
src/plugins/value/engine/analysis.ml | 4 ++++
src/plugins/value/engine/analysis.mli | 5 +++++
src/plugins/value/engine/function_calls.mli | 3 +++
3 files changed, 12 insertions(+)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 17575ba0ac3..9b43b96fa2f 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 8d06f8667a0..98c2201b905 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 3dbf96314e3..698b62406e5 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
--
GitLab