[Eva] Uses Results.are_available instead of should_memorize_function.

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)
 

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