Module verify
Source - attribute
- call_summary
- Interprocedural call summaries for the staged verifier.
- contract 🔒
- def_use
- Def-use computation for the backward path visitor.
- driver
- Driver utilities for the staged verifier pipeline.
- engine
- Shared verification engine for the staged verifier pipeline.
- generic
- Generic-parameter helpers for layout-sensitive verify checks.
- helpers 🔒
- path_extractor
- Path extraction for verification targets.
- primitive
- Primitive API classification for verifier transfer functions.
- report
- Diagnostics and summaries for the staged verifier pipeline.
- slicer
- smt_check
- SMT checking package for the staged verifier.
- target
- verifier
- Forward visitor for relevant MIR items.