Module path 

Path extraction for verification targets.

This module builds finite paths from a function CFG to each unsafe callsite. Loops are kept finite by treating a loop as a single step through one of its exits when the target callsite is outside the loop. If the target callsite is inside a loop, the path starts at the loop header and reaches the callsite within one loop iteration.

Structs

LoopExit

An edge that leaves a detected loop.

LoopId

Identifier for a detected loop in one function body.

LoopInfo

Information recorded for one detected loop.

Path

A finite verification path reaching one callsite.

PathExtractor

Extracts loop-aware paths for one function body.

PathResult

Result produced by a completed path extraction run.

SccDetector 🔒

Adapter that lets the shared SCC utility run over a MIR CFG.

Enums

LoopTransfer

Conservative summary status for a loop.

PathStart

Start point for a finite verification path.

PathStep

One step in a finite verification path.

Functions

find_loops 🔒

Detect loops in a CFG using SCCs.

has_other_callsite 🔒

Return true when block contains a non-target callsite.