From a1435a9299dfb6972acae3edede72d751a9d78f0 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 8 Mar 2024 11:59:04 -0800 Subject: [PATCH] Add comment to reverse_postorder function --- kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs index bbf5739af3e3..5fe28097a2e0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs @@ -74,6 +74,13 @@ impl<'tcx> GotocCtx<'tcx> { } } +/// Iterate over the basic blocks in reverse post-order. +/// +/// The `reverse_postorder` function used before was internal to the compiler and reflected the +/// internal body representation. +/// +/// As we introduce transformations on the top of SMIR body, there will be not guarantee of a +/// 1:1 relationship between basic blocks from internal body and monomorphic body from StableMIR. pub fn reverse_postorder(body: &Body) -> impl Iterator { postorder(body, 0, &mut HashSet::with_capacity(body.blocks.len())).into_iter().rev() }