diff --git a/src/plugins/eva/domains/domain_store.ml b/src/plugins/eva/domains/domain_store.ml index 9d8f48ecd40af05f3c35dbbe25ce5540429587d9..bdd154a2625e347f634e11e9a5b5927ae2075a4d 100644 --- a/src/plugins/eva/domains/domain_store.ml +++ b/src/plugins/eva/domains/domain_store.ml @@ -283,6 +283,12 @@ module Make (Domain: InputDomain) = struct if Storage.get () then update_callstack_table ~after:true stmt callstack state - let mark_as_computed () = Table_By_Callstack.mark_as_computed () + let mark_as_computed () = + (* Precompute consolidated states if required. *) + if Storage.get () && Parameters.JoinResults.get () then + Table_By_Callstack.iter + (fun s _ -> ignore (get_stmt_state ~after:false s)); + Table_By_Callstack.mark_as_computed () + let is_computed () = Storage.get () && Table_By_Callstack.is_computed () end diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml index e075d65bc0878adde616127d4ef1dce5e03e52ed..d46426ab057153674119cfb4d418b2a8db790894 100644 --- a/src/plugins/eva/engine/compute_functions.ml +++ b/src/plugins/eva/engine/compute_functions.ml @@ -109,10 +109,6 @@ let pre_analysis () = let post_analysis_cleanup ~aborted = Eva_utils.clear_call_stack (); - (* Precompute consolidated states if required *) - if Parameters.JoinResults.get () then - Db.Value.Table_By_Callstack.iter - (fun s _ -> ignore (Db.Value.get_stmt_state s)); if not aborted then (* Keep memexec results for users that want to resume the analysis *) Mem_exec.cleanup_results ()