From 3672747f2d4d0d015cacb6f3211a4f76dfb9a477 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 22 Feb 2022 12:21:03 +0100
Subject: [PATCH] [Eva] Uses Results.are_available instead of
should_memorize_function.
---
src/plugins/value/api/general_requests.ml | 7 +------
src/plugins/value/gui_files/gui_eval.ml | 10 +++-------
2 files changed, 4 insertions(+), 13 deletions(-)
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 4cbfd6f0af8..cb134b23ae2 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -57,12 +57,7 @@ let _computation_signal =
~add_hook:Analysis.register_computation_hook
()
-let is_computed kf =
- Analysis.is_computed () &&
- match kf with
- | { fundec = Definition (fundec, _) } ->
- Mark_noresults.should_memorize_function fundec
- | { fundec = Declaration _ } -> false
+let is_computed kf = Analysis.is_computed () && Results.are_available kf
module CallSite = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Stmt)
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index 691ec61e3e2..9264bfb5540 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -24,12 +24,8 @@ open Cil_types
open Gui_types
open Lattice_bounds
-let results_kf_computed kf =
- Analysis.is_computed () &&
- match kf with
- | { fundec = Definition (fundec, _) } ->
- Mark_noresults.should_memorize_function fundec
- | { fundec = Declaration _ } -> true (* This value is not really used *)
+let results_kf_computed kf = Analysis.is_computed () && Results.are_available kf
+let kf_called kf = Analysis.is_computed () && Results.is_called kf
let term_c_type t =
Logic_const.plain_or_set
@@ -386,7 +382,7 @@ module Make (X: Analysis.S) = struct
and correspond to the states before reduction by any precondition.
After states are not available. *)
let callstacks_at_pre kf =
- if results_kf_computed kf then
+ if kf_called kf then
let states_before = X.get_initial_state_by_callstack kf in
{ states_before; states_after = `Top }
else top_states_by_callstacks
--
GitLab