rapx 0.7.25

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
26
27
28
29
30
31
32
33

//! 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 field_invariant;
mod in_bound;
mod init;
mod non_null;
mod non_overlap;
mod non_volatile;
mod owning;
mod provenance;
mod ptr2ref;
mod transmute_without_align;
mod typed;
mod valid_cstr;
mod valid_num;
mod valid_ptr;
mod valid_transmute;

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