added initial state bdu to parallel bonds domain

Kappa-Dev · Feb 17, 2025 · a5224da · a5224da
1 parent eafafe9
commit a5224da
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/core/KaSa_rep/reachability_analysis/parallel_bonds.ml b/core/KaSa_rep/reachability_analysis/parallel_bonds.ml
@@ -17,7 +17,7 @@
 
 (** Abstract domain to over-approximate the set of reachable views *)
 
-let local_trace = true
+let local_trace = false
 
 module Domain = struct
   (* the type of the struct that contains all static information as in the

diff --git a/core/KaSa_rep/reachability_analysis/parallel_bonds_init.ml b/core/KaSa_rep/reachability_analysis/parallel_bonds_init.ml
@@ -28,8 +28,9 @@ let collect_parallel_or_not_bonds_init parameters kappa_handler bdu_handler
     Parallel_bonds_static.collect_double_bonds_in_pattern parameters error
       ?tuple_of_interest init_state.Cckappa_sig.e_init_c_mixture
   in
-  let error, bdu_handler, mvbdu_true =
-    Ckappa_sig.Views_bdu.mvbdu_true parameters bdu_handler error
+  let error, bdu_handler, mvbdu_guard =
+    Handler.guard_to_bdu_opt parameters error bdu_handler
+      init_state.Cckappa_sig.e_init_guard restriction_bdu
   in
   Parallel_bonds_static.project_away_ag_id parameters kappa_handler bdu_handler
-    error big_store store_result mvbdu_true restriction_bdu last_variable
+    error big_store store_result mvbdu_guard restriction_bdu last_variable