Enum RelevantItem 

pub enum RelevantItem<'tcx> {
    Statement {
        block: BasicBlock,
        statement_index: usize,
    },
    Terminator {
        block: BasicBlock,
    },
    ContractFact {
        property: Property<'tcx>,
    },
    Forget,
    CalleeEntry {
        callee: DefId,
        args: Vec<Local>,
    },
    CalleeExit {
        dest: Local,
    },
}

One relevant item kept from the backward slice.

Variants

Statement

A MIR statement retained from a basic block.

Fields

block: BasicBlock

statement_index: usize

Terminator

A MIR terminator retained from a basic block.

Fields

block: BasicBlock

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 (an unsupported call whose effects are not modeled).

CalleeEntry

Enter a callee’s MIR body. Subsequent Statement/Terminator items are interpreted in the callee’s context until CalleeExit. args holds the caller’s Local indices for each callee parameter (arg 0 → callee local_1, arg 1 → callee local_2, …).

Fields

callee: DefId

args: Vec<Local>

CalleeExit

Return from a callee’s MIR body. Writes local_0 (callee return) to the caller’s dest local. Restores the caller’s function context.

Fields

dest: Local

Trait Implementations

impl<'tcx> Clone for RelevantItem<'tcx>

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'tcx> Debug for RelevantItem<'tcx>

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

Formats the value using the given formatter.