Struct PrepareTargets 

pub struct PrepareTargets<'tcx> {
    tcx: TyCtxt<'tcx>,
    mode: VerifyMode,
    skip_invariant: bool,
    crate_filter: Option<String>,
    module_filter: Option<String>,
}

Analysis pass that finds all verification targets.

In targeted mode, only functions annotated with #[rapx::verify] are listed. In scan mode, all functions with unsafe callees or struct invariants are listed.

Fields

tcx: TyCtxt<'tcx>

mode: VerifyMode

skip_invariant: bool

crate_filter: Option<String>

module_filter: Option<String>

Implementations

impl<'tcx> PrepareTargets<'tcx>

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

fn log_struct_invariants(&self, struct_target: &StructTarget<'tcx>)

fn log_trait_ensurance(&self, trait_target: &TraitEnsurance<'tcx>)

fn log_method_target(&self, target: &FunctionTarget<'tcx>)

fn log_free_function_unsafe_callees(&self, target: &FunctionTarget<'tcx>)

fn log_unsafe_callees_and_contracts( &self, target: &FunctionTarget<'tcx>, path_map: &FxHashMap<DefId, Vec<(usize, Vec<String>)>>, )

fn build_checkpoint_path_map( &self, target: &FunctionTarget<'tcx>, ) -> FxHashMap<DefId, Vec<(usize, Vec<String>)>>

Trait Implementations

impl<'tcx> Analysis for PrepareTargets<'tcx>

fn run(&mut self)