From f33d6a06cf4db382eff6c4fee388a2aca5c6a8e5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 2 Aug 2023 14:18:43 +0200
Subject: [PATCH] [Eva] Precomputes the consolidated states of all domains, and
not only cvalue.
According to the -eva-join-results parameter.
---
src/plugins/eva/domains/domain_store.ml | 8 +++++++-
src/plugins/eva/engine/compute_functions.ml | 4 ----
2 files changed, 7 insertions(+), 5 deletions(-)
diff --git a/src/plugins/eva/domains/domain_store.ml b/src/plugins/eva/domains/domain_store.ml
index 9d8f48ecd40..bdd154a2625 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 e075d65bc08..d46426ab057 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 ()
--
GitLab