Module senryx 

Senryx unsafe-code soundness verification module.

The module is organized around a small set of responsibilities: driving the analysis (driver), building MIR-level state (visitor and dominated_graph), parsing contracts (contract), dispatching unsafe call-site obligations (callsite), and proving concrete safety properties (verification).

Modules

callsite 🔒

Unsafe call-site discovery and contract dispatch. Unsafe call-site contract dispatch and reporting helpers.

contract

Contract DSL and abstract-state data structures. Contract and abstract-state data types used by the Senryx verifier.

diagnostics 🔒

Result aggregation and diagnostic formatting helpers. Diagnostic and result-recording helpers for Senryx contract checks.

dominated_graph

Dominated graph model used by the MIR visitor and checkers. Dominated graph state model for Senryx MIR analysis.

driver 🔒

Top-level Senryx analysis driver. Top-level driver for Senryx verification and annotation discovery.

generic_check

Generic type candidate discovery for generic contract checks. Generic-parameter helper for Senryx layout-sensitive checks.

symbolic_analysis

Symbolic value definitions and Z3-backed proof helpers. Symbolic value domain and Z3 proof adapter for Senryx.

verification

Concrete safety-property verification procedures. Property-specific verification modules for Senryx contracts.

visitor

MIR body visitor that builds state and invokes contract checks. MIR path visitor for Senryx state construction.

Structs

SenryxCheck

Public entry points for running the Senryx analysis. Entry point for running Senryx analyses over a Rust crate.

Enums

CheckLevel

Public entry points for running the Senryx analysis. Controls how aggressively Senryx filters candidate verification targets.