charon_lib/transform/simplify_output/
update_block_indices.rs

1//! Update the block indices to make sure they are consecutive
2
3use std::mem;
4
5use crate::ids::*;
6use crate::transform::TransformCtx;
7use crate::ullbc_ast::*;
8
9use crate::transform::ctx::UllbcPass;
10
11pub struct Transform;
12impl UllbcPass for Transform {
13    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
14        // Push each block into a new vector to make it consecutive and return the map from old to
15        // new ids.
16        let id_map: Vector<BlockId, BlockId> =
17            mem::take(&mut b.body).map(|block| b.body.push(block));
18
19        // Update the ids.
20        b.body
21            .dyn_visit_in_body_mut(|id: &mut BlockId| *id = id_map[*id]);
22    }
23}