Enum ValueSource 

pub(crate) enum ValueSource<'z3> {
    None,
    FieldOffset,
    Discriminant(Int<'z3>),
    Comparison {
        lhs: Option<PlaceKey>,
        rhs: Option<PlaceKey>,
        op: BinOp,
        cond: Bool<'z3>,
    },
    BinaryOp {
        lhs: Option<PlaceKey>,
        rhs: Option<PlaceKey>,
        op: BinOp,
    },
}

The extra semantics attached to a value, beyond its term/type/provenance.

A single value carries at most one of these: it is either a plain value, an offset_of! field offset, a symbolic enum discriminant, a comparison result, or a non-comparison binary-op result. The operands/operator are used for guard inference (tracing a switch/assert guard back to the pointer it null-checks/alignment-checks) and division-axiom injection (following dataflow edges to reach Div/Rem results).

Variants

None

No extra semantics.

FieldOffset

A compile-time offset_of! field offset.

Discriminant(Int<'z3>)

A symbolic enum discriminant (variant index).

Comparison

A comparison result (Eq/Ne/Le/Lt/Ge/Gt): the operands and the direct boolean condition (offset <= len) carried alongside the ite-encoded term.

Fields

lhs: Option<PlaceKey>

rhs: Option<PlaceKey>

op: BinOp

cond: Bool<'z3>

BinaryOp

A non-comparison binary-op result (Add/Sub/…/Div/Rem): the operands and operator.

Fields

lhs: Option<PlaceKey>

rhs: Option<PlaceKey>

op: BinOp

Implementations

impl<'z3> ValueSource<'z3>

pub(crate) fn operands( &self, ) -> Option<(&Option<PlaceKey>, &Option<PlaceKey>, BinOp)>

The (lhs, rhs, op) of a binary-op/comparison result, if this value is one.

pub(crate) fn field_offset_only(&self) -> ValueSource<'z3>

Just the field-offset part of this source: FieldOffset if it is one, otherwise None.

Trait Implementations

impl<'z3> Clone for ValueSource<'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 ValueSource<'z3>

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

Formats the value using the given formatter.