Enum BackwardItem 

pub enum BackwardItem<'tcx> {
    Statement {
        block: BasicBlock,
        statement_index: usize,
        kind: KeepReason,
    },
    Terminator {
        block: BasicBlock,
        kind: KeepReason,
    },
    PathStep {
        step: PathStep,
        kind: KeepReason,
    },
    ContractFact {
        property: Property<'tcx>,
    },
    Forget {
        reason: ForgetReason,
    },
}

One item kept while walking a path backward.

Variants

Statement

A MIR statement retained from a basic block.

Fields

block: BasicBlock

statement_index: usize

kind: KeepReason

Terminator

A MIR terminator retained from a basic block.

Fields

block: BasicBlock

kind: KeepReason

PathStep

A path-level step retained as structural context.

Fields

step: PathStep

kind: KeepReason

ContractFact

A contract fact injected by the engine before the forward visit. Never produced by the backward visitor itself.

Fields

property: Property<'tcx>

Forget

A conservative loss of precision for relevant state.

Fields

reason: ForgetReason

Trait Implementations

impl<'tcx> Clone for BackwardItem<'tcx>

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'tcx> Debug for BackwardItem<'tcx>

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

Formats the value using the given formatter.