From 579f6e3d226f6c2e0017e0cf3ace6b3d28db447f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 5 Aug 2024 08:48:02 +0000 Subject: [PATCH] Actually remove insert_bb --- .../src/kani_middle/transform/body.rs | 25 ------------------- 1 file changed, 25 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index e990be330aca..56883f47b673 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -322,31 +322,6 @@ impl MutableBody { }; } - /// Insert basic block before or after the source instruction and update `source` accordingly. If - /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as - /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the - /// terminator of the newly inserted basic block. - pub fn insert_bb( - &mut self, - mut bb: BasicBlock, - source: &mut SourceInstruction, - position: InsertPosition, - ) { - // Splitting adds 1 block, so the added block index is len + 1; - let split_bb_idx = self.blocks().len(); - let inserted_bb_idx = self.blocks().len() + 1; - // Update the terminator of the basic block to point at the remaining part of the split - // basic block. - let target = get_mut_target_ref(&mut bb.terminator); - *target = split_bb_idx; - let new_term = Terminator { - kind: TerminatorKind::Goto { target: inserted_bb_idx }, - span: source.span(&self.blocks), - }; - self.split_bb(source, position, new_term); - self.blocks.push(bb); - } - pub fn insert_terminator( &mut self, source: &mut SourceInstruction,