rapx/check/senryx/
mod.rs

1//! Senryx unsafe-code soundness verification module.
2//!
3//! The module is organized around a small set of responsibilities:
4//! driving the analysis (`driver`), building MIR-level state (`visitor` and
5//! `dominated_graph`), parsing contracts (`contract`), dispatching unsafe
6//! call-site obligations (`callsite`), and proving concrete safety properties
7//! (`verification`).
8
9/// Contract DSL and abstract-state data structures.
10pub mod contract;
11/// Dominated graph model used by the MIR visitor and checkers.
12pub mod dominated_graph;
13
14/// Unsafe call-site discovery and contract dispatch.
15pub(crate) mod callsite;
16/// Result aggregation and diagnostic formatting helpers.
17mod diagnostics;
18/// Top-level Senryx analysis driver.
19mod driver;
20
21/// Generic type candidate discovery for generic contract checks.
22pub mod generic_check;
23/// Symbolic value definitions and Z3-backed proof helpers.
24pub mod symbolic_analysis;
25/// Concrete safety-property verification procedures.
26#[allow(unused)]
27pub mod verification;
28/// MIR body visitor that builds state and invokes contract checks.
29#[allow(unused)]
30pub mod visitor;
31
32/// Public entry points for running the Senryx analysis.
33pub use driver::{CheckLevel, SenryxCheck};
rapx/check/senryx/mod.rs

rapx/check/senryx/
mod.rs
