rapx 0.7.19

A static analysis platform for Rust program analysis and verification
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

//! SMT checking package for the staged verifier.
//!
//! The package is split into:
//!
//! - `common`: the shared SMT entry point, query/result types, and term model.
//! - one SP-specific module per safety property family, such as `align`.
//!
//! SP-specific modules should only lower verifier properties into common SMT
//! obligations. They should not construct independent solver APIs.

mod alias;
mod align;
mod alive;
mod allocated;
mod common;
mod deref;
mod in_bound;
mod init;
mod non_null;
mod non_overlap;
mod typed;
mod valid_num;
mod valid_ptr;

pub use common::{SmtCheckResult, SmtChecker, SmtObligation, SmtQuery};