Expand description
Concrete safety-property verification procedures. Property-specific verification modules for Senryx contracts.
The parent module only wires checker modules into the crate. Each child file
owns one safety-property family and implements the corresponding
BodyVisitor APIs used by call-site dispatch.
Modulesยง
- align
- Alignment contract checks and alignment-state refinement. Alignment contract checker for Senryx.
- bounds
- Boundary, length and zero-sized-type helper checks. Boundary and size-related contract helpers.
- init
- Initialization contract checks. Initialization contract checker.
- misc
- Miscellaneous property placeholders that still need precise models. Miscellaneous safety-property placeholders.
- non_
null - Non-null pointer checks. Non-null contract checker.
- pointer
- Composite pointer validity and dereferenceability checks. Composite pointer-safety contract checkers.
- typed
- Type-compatibility checks. Type-compatibility contract checker.