Struct VerifyRun 

pub struct VerifyRun<'tcx> {
    tcx: TyCtxt<'tcx>,
    repeat_strategy: RepeatStrategy,
    mode: VerifyMode,
    skip_invariant: bool,
    crate_filter: Option<String>,
    module_filter: Option<String>,
    debug_contracts: bool,
}

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

Fields

tcx: TyCtxt<'tcx>

repeat_strategy: RepeatStrategy

mode: VerifyMode

skip_invariant: bool

crate_filter: Option<String>

module_filter: Option<String>

debug_contracts: bool

Implementations

impl<'tcx> VerifyRun<'tcx>

pub fn new( tcx: TyCtxt<'tcx>, repeat_strategy: RepeatStrategy, mode: VerifyMode, skip_invariant: bool, crate_filter: Option<String>, module_filter: Option<String>, debug_contracts: bool, ) -> Self

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

fn repeat_rounds_for_target( &self, target: &FunctionTarget<'tcx>, ) -> (usize, Vec<usize>)

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

With --skip-invariant, 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_def_id: DefId, con_target: &FunctionTarget<'tcx>, con_id: DefId, mut_ids: &[DefId], )

impl<'tcx> VerifyRun<'tcx>

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

fn has_printable_contracts(&self, target: &FunctionTarget<'tcx>) -> bool

fn print_contract_lines( &self, prefix: &str, branch: &str, call: &str, meaning: &str, )

fn print_target_contracts( &self, target: &FunctionTarget<'tcx>, branch: &str, cont: &str, ) -> bool

fn resolve_arg_names_with_types( &self, def_id: DefId, ) -> (Vec<String>, Option<String>)

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.