Module driver 

Driver utilities for the staged verifier pipeline.

The target collector owns selected functions and their callee requirements. The path extractor upgrades a function CFG into SCC-aware path metadata. VerifyDriver prepares paths for two kinds of checks (unsafe checkpoints and struct invariants) and delegates the actual backward/forward/SMT work to the shared VerifyEngine.

Structs

CheckpointCheckView

Returns whether a function returns the owning struct type (i.e. is a constructor). Borrowed view of all verification inputs for one unsafe checkpoint.

VerifyDriver

Orchestrates the three-stage verification pipeline (backward data-dependency analysis → forward state simulation → SMT checking) for a single function under analysis.

VerifyRun

Analysis pass that runs verification and emits function-level summaries.

VerifyVisitDump

Analysis pass that dumps backward and forward visitor diagnostics.

Functions

emit_property_rows 🔒

emit_verify_summary 🔒

property_field_indices 🔒

Collect struct field indices referenced by a property’s contract places.

same_property 🔒

Return true when two properties have the same kind.

short_fn_name 🔒

Extract the last segment of a def-path (the bare function name).