Struct PrepareTargets 

pub struct PrepareTargets<'tcx> {
    tcx: TyCtxt<'tcx>,
    mode: VerifyMode,
    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

crate_filter: Option<String>

module_filter: Option<String>

Implementations

impl<'tcx> PrepareTargets<'tcx>

pub fn new( tcx: TyCtxt<'tcx>, mode: VerifyMode, 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>)

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

Trait Implementations

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

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

Return the name of the analysis.

fn run(&mut self)

Execute the analysis.

fn reset(&mut self)

Reset the analysis and cleanup the memory.