Module graph 

Structs

BlockConstantInfo

Per-block info collected during construction for path reachability analysis. Each block’s assignments, constants, and copy chains are stored together so they can be read with a single index lookup.

ComparisonSource

Records the origin of a boolean temporary produced by a binary comparison during guard-clause evaluation.

ConstraintHash

Hash of the constraint state accumulated along a path prefix.

DiscriminantInfo

Enum discriminant metadata used by [check_switch_transition].

PathEnumerator

Builds a PathTree by depth-first enumeration of whole-CFG paths.

PathGraph

CFG augmented with per-block constant info and discriminant metadata for path reachability analysis.

SccKey

Key for PathEnumerator::scc_paths and PathEnumerator::visited_sccs and PathEnumerator::visited_sccs: which SCC entry block, with what constraint state, and how many additional postfix repeats are allowed.

SccPath

A single enumerated acyclic path through an SCC region.

Constants

SCC_MAX_DEPTH 🔒

Maximum DFS depth for intra-SCC path enumeration.

SCC_MAX_PATH_LEN 🔒

Maximum path length within an SCC traversal.

SCC_MAX_SEEN_PATHS 🔒

Maximum number of distinct paths collected per SCC.

SCC_PATH_CACHE_LIMIT 🔒

Bounded cache size for SCC path enumeration.

WHOLE_CFG_PATH_DEPTH_LIMIT 🔒

Maximum DFS depth for whole-CFG path enumeration.

WHOLE_CFG_PATH_LIMIT 🔒

Maximum number of whole-CFG paths collected before stopping enumeration.

Functions

check_postfix_segment 🔒

Check whether the current entry→entry sub-path introduces a new block sequence (not just new blocks). Different branch choices inside the SCC produce different sequences even when all block IDs have already been seen, e.g. if i % 2 == 0 { A } else { B } alternates between two paths through the same set of blocks on successive loop iterations.

extract_segment 🔒

resolve_switch_target 🔒

Resolve a concrete discriminant value to the corresponding SwitchInt successor block index.