Struct ForwardVisitResult 

pub struct ForwardVisitResult<'tcx> {
    pub checkpoint: CheckpointLocation,
    pub property: Property<'tcx>,
    pub path: Path,
    pub values: FxHashMap<Local, AbstractValue<'tcx>>,
    pub value_definitions: Vec<ValueDefinition<'tcx>>,
    pub facts: Vec<StateFact<'tcx>>,
    pub forgets: Vec<ForgetReason>,
    pub steps: Vec<ForwardStep>,
    pub notes: Vec<String>,
}

Result produced by visiting relevant MIR items forward.

Fields

checkpoint: CheckpointLocation

Unsafe checkpoint being checked.

property: Property<'tcx>

Required property checked at the checkpoint.

path: Path

Path whose relevant items were visited.

values: FxHashMap<Local, AbstractValue<'tcx>>

Abstract values currently known for MIR locals.

value_definitions: Vec<ValueDefinition<'tcx>>

Path-ordered definitions produced while replaying retained MIR items.

facts: Vec<StateFact<'tcx>>

Facts recorded during the forward visit.

forgets: Vec<ForgetReason>

Places whose facts were conservatively forgotten.

steps: Vec<ForwardStep>

Ordered visit trace.

notes: Vec<String>

Unsupported items kept as notes rather than modeled facts.

Implementations

impl<'tcx> ForwardVisitResult<'tcx>

pub fn new( checkpoint: CheckpointLocation, property: Property<'tcx>, path: Path, ) -> Self

Create an empty forward visit result.

pub fn describe(&self) -> String

Render a compact diagnostic summary of this forward visit.

pub fn record_value_definition( &mut self, block: BasicBlock, statement_index: Option<usize>, local: Local, value: AbstractValue<'tcx>, )

Record one path-ordered local definition and update the final snapshot.

fn fold_self_ref( value: AbstractValue<'tcx>, local: Local, snapshot: &FxHashMap<Local, AbstractValue<'tcx>>, ) -> AbstractValue<'tcx>

Replace Place(local) inside value with the current snapshot from values. This prevents self-referencing chains when a local is re-assigned using its own previous value (e.g. i = i + 1 inside a loop).

pub fn latest_value_definition_before( &self, local: Local, cursor: usize, ) -> Option<&ValueDefinition<'tcx>>

Return the latest definition of local before the exclusive cursor.

Trait Implementations

impl<'tcx> Clone for ForwardVisitResult<'tcx>

fn clone(&self) -> ForwardVisitResult<'tcx>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'tcx> Debug for ForwardVisitResult<'tcx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.