Struct ForwardVerifier 

pub struct ForwardVerifier<'tcx> {
    tcx: TyCtxt<'tcx>,
}

Visits relevant MIR items forward and builds an abstract state.

Fields

tcx: TyCtxt<'tcx>

Implementations

impl<'tcx> ForwardVerifier<'tcx>

pub fn new(tcx: TyCtxt<'tcx>) -> Self

Create a forward visitor over the current compiler type context.

pub fn visit(&self, items: &RelevantMirItems<'tcx>) -> ForwardVisitResult<'tcx>

Visit relevant MIR items in path order and produce an abstract state.

fn visit_statement( &self, block: BasicBlock, statement_index: usize, reason: KeepReason, statement: &Statement<'tcx>, body: &Body<'tcx>, result: &mut ForwardVisitResult<'tcx>, )

Visit one retained MIR statement.

fn visit_terminator( &self, block: BasicBlock, reason: KeepReason, terminator: &Terminator<'tcx>, body: &Body<'tcx>, result: &mut ForwardVisitResult<'tcx>, )

Visit one retained MIR terminator.

fn value_from_rvalue(&self, rvalue: &Rvalue<'tcx>) -> AbstractValue<'tcx>

Build an abstract value for a MIR rvalue.

fn record_rvalue_facts( &self, block: BasicBlock, statement_index: usize, place: &Place<'tcx>, rvalue: &Rvalue<'tcx>, body: &Body<'tcx>, result: &mut ForwardVisitResult<'tcx>, )

Record initial facts directly implied by selected rvalues.

fn apply_call_effects( &self, block: BasicBlock, summary: &CallEffectSummary, args: &[Spanned<Operand<'tcx>>], is_target_checkpoint: bool, result: &mut ForwardVisitResult<'tcx>, )

Apply a summarized call effect to the path-local abstract state.

fn pointee_ty_name(&self, caller: DefId, place: &PlaceKey) -> Option<String>

Return a compact pointee type name for a raw pointer local.

fn init_write_ty_name( &self, summary: &CallEffectSummary, caller: DefId, place: &PlaceKey, ) -> String

fn allocated_element_summary( &self, caller: DefId, local: Option<Local>, ) -> Option<(String, u64)>

fn referenced_object_for_place( &self, caller: DefId, place: &Place<'tcx>, ) -> Option<PlaceKey>

fn deref_pointer_value_for_place( &self, caller: DefId, place: &Place<'tcx>, ) -> Option<PlaceKey>

fn box_projection_allocation( &self, caller: DefId, source_place: &PlaceKey, cast_ty: Ty<'tcx>, ) -> Option<(String, u64)>