Merge fixes

viperproject · Sep 27, 2023 · 185a8be · 185a8be
1 parent 491f95c
commit 185a8be
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 12 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/mir-state-analysis/src/coupling_graph/impl/engine.rs b/mir-state-analysis/src/coupling_graph/impl/engine.rs
@@ -13,12 +13,12 @@ use prusti_rustc_interface::{
         borrow_set::{BorrowData, TwoPhaseActivation},
         consumers::{Borrows, BorrowIndex, RichLocation, PlaceConflictBias, places_conflict, calculate_borrows_out_of_scope_at_location},
     },
-    dataflow::{Analysis, AnalysisDomain, CallReturnPlaces, ResultsCursor},
+    dataflow::{Analysis, AnalysisDomain, ResultsCursor},
     index::{bit_set::{BitSet, HybridBitSet}, Idx},
     middle::{
         mir::{
             TerminatorKind, Operand, ConstantKind, StatementKind, Rvalue,
-            visit::Visitor, BasicBlock, Body, Local, Place, Location, Statement, Terminator, RETURN_PLACE,
+            visit::Visitor, BasicBlock, Body, CallReturnPlaces, Local, Place, Location, Statement, Terminator, TerminatorEdges, RETURN_PLACE,
         },
         ty::{RegionVid, TyCtxt},
     },
@@ -368,12 +368,12 @@ impl<'a, 'tcx> Analysis<'tcx> for CoupligGraph<'a, 'tcx> {
         }
     }
 
-    fn apply_terminator_effect(
+    fn apply_terminator_effect<'mir>(
         &mut self,
         state: &mut Self::Domain,
-        terminator: &Terminator<'tcx>,
+        terminator: &'mir Terminator<'tcx>,
         location: Location,
-    ) {
+    ) -> TerminatorEdges<'mir, 'tcx> {
         let l = format!("{:?}", location).replace('[', "_").replace(']', "");
         // println!("Location: {l}");
         state.regions.graph.id = Some(l.clone());
@@ -434,6 +434,7 @@ impl<'a, 'tcx> Analysis<'tcx> for CoupligGraph<'a, 'tcx> {
         if cfg!(debug_assertions) && !self.repacker.body().basic_blocks[location.block].is_cleanup {
             state.regions.output_to_dot(format!("log/coupling/individual/{l}_v{}.dot", state.regions.version));
         }
+        terminator.edges()
     }
 
     fn apply_call_return_effect(

diff --git a/mir-state-analysis/src/free_pcs/impl/engine.rs b/mir-state-analysis/src/free_pcs/impl/engine.rs
@@ -5,11 +5,11 @@
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 use prusti_rustc_interface::{
-    dataflow::{Analysis, AnalysisDomain, CallReturnPlaces},
+    dataflow::{Analysis, AnalysisDomain},
     index::Idx,
     middle::{
         mir::{
-            visit::Visitor, BasicBlock, Body, Local, Location, Statement, Terminator, RETURN_PLACE,
+            visit::Visitor, BasicBlock, Body, CallReturnPlaces, Local, Location, Statement, Terminator, TerminatorEdges, RETURN_PLACE,
         },
         ty::TyCtxt,
     },
@@ -74,14 +74,15 @@ impl<'a, 'tcx> Analysis<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> {
         state.visit_statement(statement, location);
     }
 
-    fn apply_terminator_effect(
+    fn apply_terminator_effect<'mir>(
         &mut self,
         state: &mut Self::Domain,
-        terminator: &Terminator<'tcx>,
+        terminator: &'mir Terminator<'tcx>,
         location: Location,
-    ) {
+    ) -> TerminatorEdges<'mir, 'tcx> {
         state.repackings.clear();
         state.visit_terminator(terminator, location);
+        terminator.edges()
     }
 
     fn apply_call_return_effect(

diff --git a/mir-state-analysis/src/free_pcs/impl/triple.rs b/mir-state-analysis/src/free_pcs/impl/triple.rs
@@ -69,8 +69,8 @@ impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> {
         match &terminator.kind {
             Goto { .. }
             | SwitchInt { .. }
-            | Resume
-            | Terminate
+            | UnwindResume
+            | UnwindTerminate(_)
             | Unreachable
             | Assert { .. }
             | GeneratorDrop