Struct PathFacts 

pub(crate) struct PathFacts {
    pub reenter: bool,
    pub split_transmute_asserted: bool,
    pub alias_hazard_accepted: bool,
    pub has_checked_bounds: bool,
    pub saw_next_discriminant: bool,
}

Per-path facts, read afterwards by the property checker.

Most flags are latched at most once during path execution (a contract fact or a recognized discriminant / bounds check); reenter is instead derived from the input path in VmState::new. They are per-path state, not per-step: once set they are never cleared within a path. (has_checked_bounds is additionally accumulated across checkpoints by the engine, which reads it back into the next path’s flags.)

Fields

reenter: bool

Whether the current path re-enters a block (loop-unrolled), which lets the checker exempt the unrolled iteration’s “second drop”.

split_transmute_asserted: bool

Whether a SplitTransmute contract was asserted by the caller.

alias_hazard_accepted: bool

Whether an Alias hazard was accepted via the caller’s contract.

has_checked_bounds: bool

Whether a ChecksIndexBoundsDisjoint call was processed in any checkpoint of this function (accumulated across checkpoints).

saw_next_discriminant: bool

Set once the path evaluated an Iterator::next discriminant whose variant was known symbolically.

Trait Implementations

impl Clone for PathFacts

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for PathFacts

impl Debug for PathFacts

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

Formats the value using the given formatter.

impl Default for PathFacts

fn default() -> Self

Returns the “default value” for a type.