Module scc

Module scc 

Source
Expand description

Shared strongly-connected-component utilities.

This module provides the small Tarjan SCC abstraction used by RAPx analyses and by the verification path extractor. The trait is intentionally graph agnostic: clients provide successor queries and receive each discovered SCC through on_scc_found.

Structs§

SccComponentCollector 🔒
SccExit
An outgoing edge from an SCC body to a block outside the SCC.
SccInfo
Per-header SCC metadata used by loop-aware analyses.
SccRegion
A cyclic SCC region specialized for MIR basic blocks.
SccRegionExit
An edge that leaves a detected MIR SCC region.

Traits§

Scc
Tarjan SCC callback trait.

Functions§

collect_scc_components
Collect all SCC components from a successor graph.
find_scc_regions
Detect cyclic SCC regions in a MIR CFG successor graph.