Enum RelevantItem 

pub(crate) enum RelevantItem<'tcx> {
    Statement {
        def_id: DefId,
        block: BasicBlock,
        statement_index: usize,
    },
    Terminator {
        def_id: DefId,
        block: BasicBlock,
        switch_succ: Option<BasicBlock>,
    },
    CalleeEntry {
        callee: DefId,
        args: Vec<usize>,
    },
    CalleeExit {
        dest: usize,
    },
    ContractFact {
        property: Property<'tcx>,
    },
    UnknownCall,
}

One relevant item kept from the backward slice.

Variants

Statement

A MIR statement retained from a basic block. def_id identifies the function owning block (differs from the caller for inlined callees).

Fields

def_id: DefId

block: BasicBlock

statement_index: usize

Terminator

A MIR terminator retained from a basic block. For a SwitchInt, block is the switch block and switch_succ is the successor taken along this path (so the VM need not re-resolve it from the path); for any other terminator — or when the path ends at the checkpoint — switch_succ is None.

Fields

def_id: DefId

block: BasicBlock

switch_succ: Option<BasicBlock>

CalleeEntry

Enter an inlined callee: bind the caller’s argument locals to the callee parameters. args holds the caller’s argument local indices.

Fields

callee: DefId

args: Vec<usize>

CalleeExit

Return from an inlined callee: write the callee’s _0 to the caller’s destination local.

Fields

dest: usize

ContractFact

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

Fields

property: Property<'tcx>

UnknownCall

An unknown call with no summary (unsupported): its effects cannot be modeled, so the slicer keeps the terminator but conservatively drops precision on the relevant state it touches. The forward VM is a no-op on this marker.

Trait Implementations

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

fn clone(&self) -> Self

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.