From 9e172424cbe5d6e645cf71241f49b7344d9ae1d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 13 Apr 2022 15:54:40 +0200
Subject: [PATCH] [Eva] Fixes API results on functions interpreted by a builtin
or a specification.
Returns `Bottom instead of `Top at any statement of such functions.
In particular, [is_reachable stmt] is false for these statements.
---
src/plugins/value/engine/analysis.ml | 4 ++--
src/plugins/value/engine/analysis.mli | 4 ++--
src/plugins/value/utils/results.mli | 2 +-
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index a34af07d560..11e429d42db 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -100,8 +100,8 @@ module Make (Abstract: Abstractions.S) = struct
then
let kf = Kernel_function.find_englobing_kf stmt in
match status kf with
- | Unreachable -> `Bottom
- | Analyzed NoResults | SpecUsed | Builtin _ -> `Top
+ | Unreachable | SpecUsed | Builtin _ -> `Bottom
+ | Analyzed NoResults -> `Top
| Analyzed (Complete | Partial) -> f stmt
else `Top
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index c4fb144b74a..789e4837586 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -128,11 +128,11 @@ type status =
| SpecUsed
(** The function specification has been used to interpret its calls:
its body has not been analyzed. Any request at a statement of this
- function will lead to a Top result. *)
+ function will lead to a Bottom result. *)
| Builtin of string
(** The builtin of the given name has been used to interpret the function:
its body has not been analyzed. Any request at a statement of this
- function will lead to a Top result. *)
+ function will lead to a Bottom result. *)
| Analyzed of results
(** The function body has been analyzed. *)
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index fac0e191f42..de423c3260f 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -60,7 +60,7 @@
- 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.
+ function body: all requests in the function will lead to a Bottom 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
--
GitLab