charon_lib::transform::ullbc_to_llbc

Function can_reach_outer_exit

source
fn can_reach_outer_exit(
    cfg: &CfgInfo,
    outer_exits: &HashSet<BlockId>,
    start_bid: BlockId,
    exit_candidate: BlockId,
) -> bool
Expand description

Auxiliary helper

Check if it is possible to reach the exit of an outer switch from [bid] without going through the [exit_candidate]. We use the graph without backward edges.