Module path_extractor 

Path extraction for verification targets.

This module builds finite, acyclic paths from a function CFG to each unsafe checkpoint so that the verifier can reason about pointer properties along concrete execution traces without unrolling loops or recursive cycles.

Path reachability

Each path is validated against a PathGraph (an SCC-aware path enumeration structure) to ensure the computed block sequence is actually reachable. Paths that fail this check are silently discarded.

Path limit

To prevent exponential blow-up, path enumeration is capped at crate::limit::path_limit (the --path-limit CLI value, or crate::limit::PATH_LIMIT). Enumeration stops producing new paths once the limit is reached and the tree is marked truncated.

Structs

CallGroup 🔒

Checkpoints targeting the same callee, grouped for shared path analysis.

Path 🔒

One finite, acyclic execution trace from the function entry to a target checkpoint, represented as an ordered sequence of MIR basic blocks.

PathExtractor 🔒

Enumerates finite, SCC-aware verification paths from the function entry to each unsafe checkpoint in a single function body.

Enums

PathStep 🔒

One step in a finite verification path.

Functions

group_by_callee 🔒