From 4bb2031361936b8b6107ebdb833927397c4e26ac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 22 Feb 2022 10:43:03 +0100
Subject: [PATCH] [Eva] API: exports [use_spec_instead_of_definition].
---
src/plugins/value/engine/analysis.ml | 3 +++
src/plugins/value/engine/analysis.mli | 6 ++++++
2 files changed, 9 insertions(+)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index f8adbfbb0d2..17575ba0ac3 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -208,3 +208,6 @@ 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
+
+let use_spec_instead_of_definition =
+ Function_calls.use_spec_instead_of_definition ?recursion_depth:None
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index e74658ef216..8d06f8667a0 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -138,6 +138,12 @@ type status =
(** Returns the analysis status of a given function. *)
val status: Cil_types.kernel_function -> status
+
+(** Does the analysis ignores the body of a given function, and uses instead
+ its specification or a builtin to interpret it?
+ 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
[@@@ api_end]
val cvalue_initial_state: unit -> Cvalue.Model.t
--
GitLab