diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml index 4cbfd6f0af85695976d06833b4e2871f6110b76b..cb134b23ae25a20ef3a1b497dbc6ba62a148fc20 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 691ec61e3e21054da275d86deaf89cf264b1147a..9264bfb55403509312c971ee1ea1b614d1381777 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