Struct ValueFacts 

pub(crate) struct ValueFacts<'z3> {
    pub non_null: bool,
    pub init: bool,
    pub in_bounds: bool,
    pub align_n: Option<Int<'z3>>,
}

Value-level facts about a single symbolic value (nullness, alignment, bounds, and whether it has been written). These travel with the value — a VmValue leaves its allocation when passed as an operand or stashed in InlineCtx::deferred_field_writes — so they live on the value, not the allocation. The allocation-level counterpart to init is ContentFacts::initialized, kept in sync by VmState::mark_initialized.

PartialEq/Eq are deliberately not derived: align_n is a Z3 AST whose equality is structural (Z3_is_eq_ast), not semantic, so comparing two ValueFacts would silently report semantically-equal values as unequal.

Fields

non_null: bool

init: bool

in_bounds: bool

align_n: Option<Int<'z3>>

If Some(n), the value’s term is known to satisfy z3_term % n == 0. Set by alignment guards, Mul by power-of-two, and type alignment. n is a Z3 term so that a generic type’s alignment (a symbolic align_T) can be carried the same way as a concrete alignment.

Trait Implementations

impl<'z3> Clone for ValueFacts<'z3>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'z3> Debug for ValueFacts<'z3>

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

Formats the value using the given formatter.

impl<'z3> Default for ValueFacts<'z3>

fn default() -> Self

Returns the “default value” for a type.

impl Display for ValueFacts<'_>

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

Formats the value using the given formatter.