Struct PropertyCheckResult 

pub struct PropertyCheckResult<'tcx> {
    pub checkpoint: CheckpointLocation,
    pub checkpoint_index: usize,
    pub path_index: usize,
    pub property_index: usize,
    pub property: Property<'tcx>,
    pub result: CheckResult,
    pub diagnostics: Option<VisitDiagnostics>,
    pub path_description: String,
    pub callee_name: String,
}

Result for one required property along one path to a checkpoint.

Fields

checkpoint: CheckpointLocation

Unsafe checkpoint being checked.

checkpoint_index: usize

Index of the checkpoint in the function-level checkpoint list.

path_index: usize

Index of the path in the checkpoint path set.

property_index: usize

Index of the property in the checkpoint-level property list.

property: Property<'tcx>

Required property checked on this path.

result: CheckResult

Current verification status.

diagnostics: Option<VisitDiagnostics>

Optional path-local diagnostics generated by the staged visitors.

path_description: String

Human-readable path description.

callee_name: String

Callee name for this checkpoint.

Trait Implementations

impl<'tcx> Clone for PropertyCheckResult<'tcx>

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'tcx> Debug for PropertyCheckResult<'tcx>

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

Formats the value using the given formatter.