rapx 0.7.39

A static analysis platform for Rust program analysis and verification
1
2
3
4
5
6
7
8
9
10
11
12

//! Backward data-dependency slicer.
//!
//! Given a path tree, a checkpoint, and a property, it walks each path backward
//! to keep only the MIR items that are data-relevant to the property, producing
//! one [`ProofGoal`] per path for the symbolic VM to execute forward.

mod call_visit;
pub(crate) mod types;
mod visitor;

pub(crate) use types::{ProofGoal, RelevantItem};
pub(crate) use visitor::BackwardSlicer;