Expand description
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§
- Checkpoint
Check View - Returns whether a function returns the owning struct type (i.e. is a constructor). Borrowed view of all verification inputs for one unsafe checkpoint.
- Verify
Driver - Orchestrates the three-stage verification pipeline (backward data-dependency analysis → forward state simulation → SMT checking) for a single function under analysis.
- Verify
Run - Analysis pass that runs verification and emits function-level summaries.
Functions§
- property_
field_ 🔒indices - Return true when two properties have the same kind. Collect struct field indices referenced by a property’s contract places.
- remap_
constructor_ 🔒contract