rapx/verify/slicer/mod.rs
1//! Backward data-dependency slicer.
2//!
3//! Given a path tree, a checkpoint, and a property, it walks each path backward
4//! to keep only the MIR items that are data-relevant to the property, producing
5//! one [`ProofGoal`] per path for the symbolic VM to execute forward.
6
7mod call_visit;
8pub(crate) mod types;
9mod visitor;
10
11pub(crate) use types::{ProofGoal, RelevantItem};
12pub(crate) use visitor::BackwardSlicer;