charon_lib::transform::ullbc_to_llbc

Function compute_switch_exits_explore

source 
fn compute_switch_exits_explore(
    cfg: &CfgInfo,
    tsort_map: &HashMap<BlockId, usize>,
    memoized: &mut HashMap<BlockId, BlocksInfo>,
    block_id: BlockId,
) -> BlocksInfo
Expand description

Compute BlocksInfo for every block in the graph. This information is then used to compute the switch exits.