rapx 0.7.40

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

//! The staged verification pipeline.
//!
//! Contract-based, path-sensitive verification of safety properties: collect
//! targets and contracts, extract SCC-aware paths, slice them backward, execute
//! the relevant MIR symbolically, and discharge each property with Z3.

pub(crate) mod api_classify;
pub(crate) mod call_summary;
pub(crate) mod contract;
pub(crate) mod def_use;
pub(crate) mod display;
pub(crate) mod driver;
pub(crate) mod engine;
pub(crate) mod loop_sensitivity;
pub(crate) mod path_extractor;

pub(crate) mod property_checker;
pub(crate) mod report;
pub(crate) mod slicer;
pub(crate) mod target;
pub(crate) mod type_invariants;

pub(crate) mod vm;