Skip to main content

path_infeasible_under_context

rapx::verify::call_summary::interprocedural

Function path_infeasible_under_context 

Source 
fn path_infeasible_under_context(
    body: &Body<'_>,
    path: &[usize],
    context: &CallContext,
) -> bool
Expand description

Return true if path is provably infeasible under context, by folding a SwitchInt whose discriminant is a direct copy of a concrete argument. Only prunes when the taken target is uniquely determined, so a feasible path is never removed.