Module limit 

Central home for every numeric limit / bound used across the analysis and verification pipeline.

Before this module, each limit lived as a module-local const/static next to its consumer, so thresholds were duplicated (the 16-block inline cap appeared in both the path graph and the runtime inliner) and hard to audit. Keeping them all here mirrors crate::def_id: one flat, well-documented location where a knob can be found and tuned without grepping the crate.

Everything is pub(crate); names that would otherwise collide across modules (the two VISIT_LIMITs, the two MAX_DEPTHs) are prefixed with their owning analysis.

Constants

ALIAS_VISIT_LIMIT 🔒

Visit cap for the alias-graph DFS/iteration in the default alias analysis.

DEFAULT_LOOP_CARRIED_BACKEDGES 🔒

Fallback loop-carried distance used when a sink is loop-sensitive but the local transfer graph is too imprecise to calculate a better distance.

DEFAULT_NUMERIC_WITNESS_ITERATION 🔒

Conservative first numeric witness when an index obligation is known to be induction-sensitive but the current summary cannot yet recover a concrete symbolic bound.

FIELD_LOAD_EFFECT_BLOCK_LIMIT 🔒

Max basic-block count for a local callee to be recognized as a pure field-load (_0 = (*_1).field) summary.

FROM_RAW_PARTS_WRAPPER_BLOCK_LIMIT 🔒

Max basic-block count for a local callee to be recognized as a from_raw_parts wrapper summary.

FUZZABLE_MAX_DEPTH 🔒

Recursion depth cap for the fuzzable-type predicate.

LOCAL_INLINE_BLOCK_LIMIT 🔒

A local callee is inlined into the path CFG only when its MIR is at most this many basic blocks. This is a transitive shape bound: local inlining recurses into the callee’s own calls, so every inlined body multiplies the path-graph size. Cross-crate callees are exempt — they are inlined a single level and never recursed into, so their size is not bounded here.

MAX_AUTO_REPEAT 🔒

Caps how many times a loop body is unrolled during path enumeration; loop-heavy functions (e.g. UTF-16 decoders) scale super-linearly with it. Lower it to speed up verification at the cost of loop sensitivity (bugs that only manifest after more iterations can be missed).

MAX_DEREF_DEPTH 🔒

Recursion cap on nested dereferences while building a points-to graph.

MAX_FIELD_DEPTH 🔒

Recursion cap on nested field projection while building a points-to graph.

MAX_INLINE_DEPTH 🔒

Recursion depth bound for runtime inlining ([crate::verify::vm::call::exec_inline_call]). Recursive inlining unwinds through the Rust call stack, so this caps nesting.

MAX_STEP_SET_SIZE 🔒

Cap on the number of monomorphization steps retained per API-dependency resolution.

MAX_TY_COMPLX 🔒

Upper bound on type complexity accepted when resolving API-dependency output types.

MAX_VALUES_PER_PATH 🔒

Hard cap on the number of values a single points-to path may materialize.

MIN_DATAFLOW_REPEAT 🔒

The first repeat depth that reliably exposes the existing delayed loop-carried pointer/state fixtures.

PATH_LIMIT 🔒

Maximum number of paths collected per search — both whole-CFG enumeration and per-checkpoint prefix collection. Overridable via the --path-limit CLI flag.

POINTER_ARITH_WRAPPER_BLOCK_LIMIT 🔒

Max basic-block count for a local callee to be recognized as a pointer-arithmetic (add/sub) wrapper summary.

SAFEDROP_VISIT_LIMIT 🔒

Visit cap for the SafeDrop graph DFS.

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.

SLICE_BOUNDED_RETURN_BLOCK_LIMIT 🔒

Max basic-block count for a local callee to be recognized as a slice-bounded return summary.

WHOLE_CFG_PATH_DEPTH_LIMIT 🔒

Maximum DFS depth for whole-CFG path enumeration.

Statics

PATH_LIMIT_OVERRIDE 🔒

Runtime override for PATH_LIMIT, set from --path-limit. 0 means “not overridden” (the default above applies).

Functions

path_limit 🔒

The effective path cap (override, or PATH_LIMIT).

set_path_limit 🔒

Set the --path-limit override; 0 restores PATH_LIMIT.