Struct Path 

pub struct Path {
    pub target: CheckpointLocation,
    pub steps: Vec<PathStep>,
}

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

A Path is the core currency flowing through the verification pipeline. It is produced by PathExtractor, then consumed by the BackwardSlicer to determine which MIR instructions are relevant to the safety property being checked.

Structure

Each path consists of:

• target — the CheckpointLocation identifying the specific call terminator (or synthetic checkpoint) this path reaches. Redundant with the final step but stored separately for fast lookup.
• steps — an ordered list of PathStep values. Intermediate steps are MIR basic blocks; the final step is always PathStep::Checkpoint(target). The path always starts at function entry (block bb0).

Reachability

Every Path returned by PathExtractor is guaranteed to be reachable in the function’s CFG. Paths that cannot be validated against the SCC-aware PathGraph are silently discarded during extraction.

Example (compact notation)

bb2 -> bb3 -> bb4 -> checkpoint@bb5::unsafe_fn

In the path above, blocks 2, 3, and 4 are intermediate MIR blocks; block 5 contains the unsafecall terminator that the path targets.

Fields

target: CheckpointLocation

The checkpoint location (function + basic block) reached by this path.

steps: Vec<PathStep>

Ordered sequence of basic blocks from function entry to target, terminated by a PathStep::Checkpoint.

Implementations

impl Path

pub fn describe(&self) -> String

Render this path as a compact string for diagnostics.

pub fn describe_body(&self) -> String

Render only the path body from the start point to the checkpoint.

pub fn describe_indices(&self) -> String

Render this path as a compact array of block indices.

Trait Implementations

impl Clone for Path

fn clone(&self) -> Path

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Path

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.