Expand description
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 PATH_LIMIT
(currently 1024) per search. Searches stop producing new paths once the limit
is reached.
Structs§
- Call
Group - 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.
- Path
Extractor - Enumerates finite, SCC-aware verification paths from the function entry to each unsafe checkpoint in a single function body.
Enums§
- Path
Step - One step in a finite verification path.