[Eva] Iterator: save results according to [Function_calls.define_analysis_target].

src/plugins/value/engine/compute_functions.ml

@@ -212,8 +212,8 @@ module Make (Abstract: Abstractions.Eva) = struct
 
   (* Interprets a [call] at callsite [kinstr] in the state [state] by analyzing
      the body of the called function. *)
-  let compute_using_body fundec kinstr call state =
-    let result = Computer.compute call.kf kinstr state in
+  let compute_using_body fundec ~save_results kinstr call state =
+    let result = Computer.compute ~save_results call.kf kinstr state in
     Summary.FunctionStats.recompute fundec;
     result
 
@@ -246,8 +246,10 @@ module Make (Abstract: Abstractions.Eva) = struct
     let call_stack = Eva_utils.call_stack () in
     let compute, kind =
       match target with
-      | `Def (fundec, _) -> compute_using_body fundec, `Def
-      | `Spec funspec -> compute_using_spec funspec, `Spec funspec
+      | `Def (fundec, save_results) ->
+        compute_using_body fundec ~save_results, `Def
+      | `Spec funspec ->
+        compute_using_spec funspec, `Spec funspec
     in
     Db.Value.Call_Type_Value_Callbacks.apply (kind, cvalue_state, call_stack);
     let resulting_states, cacheable = compute kinstr call state in

src/plugins/value/engine/function_calls.mli

@@ -25,7 +25,8 @@ open Cil_types
 (** What is used for the analysis of a given function:
     - a Cvalue builtin (and other domains use the specification)
     - the function specification
-    - the function body. *)
+    - the function body. The boolean indicates whether the resulting states
+      must be recorded at each statement of this function. *)
 type analysis_target =
   [ `Builtin of string * Builtins.builtin * Eval.cacheable * funspec
   | `Spec of Cil_types.funspec

src/plugins/value/engine/iterator.ml

@@ -667,7 +667,7 @@ module Make_Dataflow
     );
     states_after
 
-  let merge_results () =
+  let merge_results ~save_results =
     let get_merged_states =
       let merged_states = VertexTable.create control_point_count
       and get_smashed_store v =
@@ -700,7 +700,7 @@ module Make_Dataflow
     let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
     and merged_post_cvalues = lazy (lift_to_cvalues merged_post_states) in
     let callstack = Eva_utils.call_stack () in
-    if Mark_noresults.should_memorize_function fundec then begin
+    if save_results then begin
       let register_pre = Domain.Store.register_state_before_stmt callstack
       and register_post = Domain.Store.register_state_after_stmt callstack in
       StmtTable.iter register_pre (Lazy.force merged_pre_states);
@@ -762,7 +762,7 @@ module Computer
      end)
 = struct
 
-  let compute kf call_kinstr state =
+  let compute ~save_results kf call_kinstr state =
     let module Dataflow =
       Make_Dataflow
         (Abstract) (States) (Transfer) (Init) (Logic) (Spec)
@@ -778,7 +778,7 @@ module Computer
       if Parameters.ValShowProgress.get () then
         Self.feedback "Recording results for %a"
           Kernel_function.pretty kf;
-      Dataflow.merge_results ();
+      Dataflow.merge_results ~save_results;
       let f = Kernel_function.get_definition kf in
       if Cil.hasAttribute "noreturn" f.svar.vattr && results <> [] then
         Eva_utils.warning_once_current
@@ -788,7 +788,7 @@ module Computer
     in
     let cleanup () =
       Dataflow.mark_degeneration ();
-      Dataflow.merge_results ()
+      Dataflow.merge_results ~save_results
     in
     Eva_utils.protect compute ~cleanup
 end

src/plugins/value/engine/iterator.mli

@@ -44,6 +44,7 @@ module Computer
   : sig
 
     val compute:
+      save_results:bool ->
       kernel_function -> kinstr -> Abstract.Dom.t ->
       (Partition.key * Abstract.Dom.t) list * Eval.cacheable