Struct VerifyRun 

pub struct VerifyRun<'tcx> {
    tcx: TyCtxt<'tcx>,
    postfix_repeat: usize,
    mode: VerifyMode,
    crate_filter: Option<String>,
    module_filter: Option<String>,
}

Analysis pass that runs verification and emits function-level summaries.

Fields

tcx: TyCtxt<'tcx>

postfix_repeat: usize

mode: VerifyMode

crate_filter: Option<String>

module_filter: Option<String>

Implementations

impl<'tcx> VerifyRun<'tcx>

pub fn new( tcx: TyCtxt<'tcx>, postfix_repeat: usize, mode: VerifyMode, crate_filter: Option<String>, module_filter: Option<String>, ) -> Self

Create the default verify pass for the current compiler type context.

fn run_invless_sequences(&self, targets: &[FunctionTarget<'tcx>])

In invless mode, generate verification sequences for each read method that chain through constructors and mutators.

Produces sequences like:

• constructor → method
• constructor → mutator → method

Each sequence propagates the constructor’s #[rapx::requires] through the mutator chain to serve as entry assumptions for the read method.

fn build_virtual_target( &self, read_target: &FunctionTarget<'tcx>, read_def_id: DefId, con_id: DefId, mut_ids: &[DefId], ) -> FunctionTarget<'tcx>

fn verify_and_emit_sequence( &self, _read_target: &FunctionTarget<'tcx>, read_def_id: DefId, con_target: &FunctionTarget<'tcx>, con_id: DefId, mut_ids: &[DefId], _seq_index: usize, )

Trait Implementations

impl<'tcx> Analysis for VerifyRun<'tcx>

fn run(&mut self)

Collect verify targets, run the staged driver, and emit a compact summary.

For each target, extracts paths with increasing postfix-repeat levels from 0 to the configured maximum, running verification at each level. Earlier rounds use fewer loop unrollings; later rounds incrementally add deeper paths.

fn name(&self) -> &'static str

Return the name of the analysis.

fn reset(&mut self)

Reset the analysis and cleanup the memory.