rapx/check/senryx/verification/
mod.rs

1//! Property-specific verification modules for Senryx contracts.
2//!
3//! The parent module only wires checker modules into the crate. Each child file
4//! owns one safety-property family and implements the corresponding
5//! `BodyVisitor` APIs used by call-site dispatch.
6
7/// Alignment contract checks and alignment-state refinement.
8pub mod align;
9/// Boundary, length and zero-sized-type helper checks.
10pub mod bounds;
11/// Initialization contract checks.
12pub mod init;
13/// Miscellaneous property placeholders that still need precise models.
14pub mod misc;
15/// Non-null pointer checks.
16pub mod non_null;
17/// Composite pointer validity and dereferenceability checks.
18pub mod pointer;
19/// Type-compatibility checks.
20pub mod typed;