Fix some issues

viperproject · Feb 13, 2025 · 805c79e · 805c79e
1 parent bf896be
commit 805c79e
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/src/free_pcs/results/cursor.rs b/src/free_pcs/results/cursor.rs
@@ -88,11 +88,11 @@ impl<'mir, 'tcx, D: HasPcg<'mir, 'tcx>, E: Analysis<'tcx, Domain = D>>
 
         let state = self.cursor.get();
 
-        let prev_post_main = state.get_curr_fpcg().post_main().clone();
-
         self.cursor.seek_after_primary_effect(location);
 
+
         let state = self.cursor.get();
+        let prev_post_main = state.get_curr_fpcg().data.entry_state.clone();
         let curr_fpcs = state.get_curr_fpcg();
         let curr_borrows = state.get_curr_borrow_pcg();
         let repack_ops = curr_fpcs.repack_ops(&prev_post_main).unwrap_or_else(|e| {

diff --git a/src/utils/domain_data.rs b/src/utils/domain_data.rs
@@ -46,6 +46,8 @@ impl<T: Clone + Default> DomainData<T> {
             // The entry state may have taken into account previous joins
             self.states.post_main = self.entry_state.clone();
             self.phase = DataflowPhase::Transfer;
+        } else {
+            self.entry_state = self.states.post_main.clone();
         }
     }
     pub(crate) fn enter_join(&mut self) {