Struct Checkpoint 

pub struct Checkpoint<'tcx> {
    pub caller: DefId,
    pub callee: Option<DefId>,
    pub block: BasicBlock,
    pub args: Vec<Operand<'tcx>>,
    pub kind: CheckpointKind,
    pub destination: Option<Local>,
    pub is_mut_ref: bool,
    pub statement_index: usize,
}

A verification checkpoint in one MIR body.

Unifies unsafe calls, raw-pointer dereferences, and mutable static accesses under a single type so they all flow through the same path extraction and SMT verification pipeline.

Fields

caller: DefId

callee: Option<DefId>

block: BasicBlock

args: Vec<Operand<'tcx>>

kind: CheckpointKind

destination: Option<Local>

is_mut_ref: bool

For RawPtrDeref checkpoints: whether the deref produces a mutable reference (&mut *ptr) rather than a shared one (&*ptr).

statement_index: usize

For RawPtrDeref checkpoints: statement index within block, used for reverse liveness at the deref point.

Implementations

impl<'tcx> Checkpoint<'tcx>

pub fn location(&self) -> CheckpointLocation

Return the MIR location that identifies this checkpoint inside the verifier.

pub fn callee_name(&self, tcx: TyCtxt<'tcx>) -> String

Return a human-readable label for diagnostics.

Trait Implementations

impl<'tcx> Clone for Checkpoint<'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 Checkpoint<'tcx>

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

Formats the value using the given formatter.