Slightly less hacky way to satisfy borrow checker

model-checking · Jul 16, 2024 · 4047006 · 4047006
1 parent f12b36d
commit 4047006
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 deletions.
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
@@ -193,9 +193,7 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> {
                 self.call_graph.add_edges(to_visit, &next_items);
 
                 self.queue.extend(next_items.into_iter().filter_map(
-                    |CollectedItem { item, .. }| {
-     (!self.collected.contains(&item)).then_some(item)
-                    },
+                    |CollectedItem { item, .. }| (!self.collected.contains(&item)).then_some(item),
                 ));
             }
         }

diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs
@@ -136,11 +136,11 @@ impl BodyTransformation {
         instances: Vec<Instance>,
         call_graph: CallGraph,
     ) {
-        let mut global_passes: Vec<_> = self.global_passes.drain(0..).collect();
+        let mut global_passes = std::mem::take(&mut self.global_passes);
         for global_pass in global_passes.iter_mut() {
             global_pass.transform(tcx, &call_graph, starting_items, instances.clone(), self);
         }
-        self.global_passes.extend(global_passes);
+        std::mem::swap(&mut self.global_passes, &mut global_passes);
     }
 
     fn add_pass<P: TransformPass + 'static>(&mut self, query_db: &QueryDb, pass: P) {