Enum SmtObligation 

pub enum SmtObligation {
    Aligned {
        place: PlaceKey,
        align: u64,
        ty_name: String,
    },
    NonZero {
        place: PlaceKey,
    },
    Range {
        value: PlaceKey,
        lower: i128,
        upper: Option<i128>,
    },
    InBounds {
        place: PlaceKey,
        ty_name: String,
        elem_size: u64,
        access_count: SmtTerm,
    },
    PointerRangeInBounds {
        place: PlaceKey,
        ty_name: String,
        lower_delta: SmtTerm,
        upper_delta: SmtTerm,
    },
    Initialized {
        place: PlaceKey,
        ty_name: String,
        elements: SmtTerm,
        elem_size: Option<u64>,
        array_elem_size: Option<u64>,
        array_len_term: Option<SmtTerm>,
    },
    Allocated {
        place: PlaceKey,
        ty_name: String,
        elements: SmtTerm,
    },
    NonOverlapping {
        left: PlaceKey,
        right: PlaceKey,
        left_count: SmtTerm,
        right_count: SmtTerm,
        elem_size: u64,
    },
    Predicate {
        predicates: Vec<SmtPredicate>,
    },
}

General SMT obligation produced by an SP-specific lowering.

Variants

Aligned

Prove that the address denoted by place is aligned to align bytes.

Fields

place: PlaceKey

align: u64

ty_name: String

NonZero

Future form for non-zero integer/address requirements.

Fields

place: PlaceKey

Range

Future form for interval/bounds requirements.

Fields

value: PlaceKey

lower: i128

upper: Option<i128>

InBounds

Prove that place points to access_count elements inside its object.

Fields

place: PlaceKey

ty_name: String

elem_size: u64

access_count: SmtTerm

PointerRangeInBounds

Prove that pointer arithmetic starting at place stays inside the matched object for the whole delta range.

Fields

place: PlaceKey

ty_name: String

lower_delta: SmtTerm

upper_delta: SmtTerm

Initialized

Prove that place denotes initialized memory for elements elements.

Fields

place: PlaceKey

ty_name: String

elements: SmtTerm

elem_size: Option<u64>

Byte size of one element of the required type (None = unknown).

array_elem_size: Option<u64>

Per-element size of the inner array element type.

array_len_term: Option<SmtTerm>

SMT term for the array length const-generic (when type is [T; N]).

Allocated

Prove that place points to elements elements in one live allocation.

Fields

place: PlaceKey

ty_name: String

elements: SmtTerm

NonOverlapping

Prove that two pointer ranges do not overlap.

Fields

left: PlaceKey

right: PlaceKey

left_count: SmtTerm

right_count: SmtTerm

elem_size: u64

Predicate

Prove one or more numeric predicates.

Fields

predicates: Vec<SmtPredicate>

Implementations

impl SmtObligation

pub fn describe(&self) -> String

Render a compact obligation description for diagnostics.

Trait Implementations

impl Clone for SmtObligation

fn clone(&self) -> SmtObligation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SmtObligation

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

Formats the value using the given formatter.