Struct Checkpoint 

pub struct Checkpoint<'tcx> {
    pub caller: DefId,
    pub callee: Option<DefId>,
    pub block: BasicBlock,
    pub span: Span,
    pub args: Vec<Operand<'tcx>>,
    pub kind: CheckpointKind,
    pub is_ref: bool,
}

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

span: Span

args: Vec<Operand<'tcx>>

kind: CheckpointKind

is_ref: bool

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) -> Checkpoint<'tcx>

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.