Enum CallEffect 

pub enum CallEffect {
    ReturnAliasArg {
        arg: usize,
    },
    ReturnPointerFromArg {
        arg: usize,
    },
    ReturnPointerAdd {
        base_arg: usize,
        offset_arg: usize,
        stride: Option<u64>,
    },
    ReturnPointerSub {
        base_arg: usize,
        offset_arg: usize,
        stride: Option<u64>,
    },
    ReturnNonZero,
    ReturnAligned {
        align: u64,
        ty_name: String,
    },
    ReturnConst {
        value: u64,
        label: String,
    },
    ReadMemory {
        arg: usize,
    },
    WriteMemory {
        pointer_arg: usize,
    },
    ReturnFreshAllocation {
        pointer_arg: usize,
        size_arg: usize,
        elem_size: u64,
    },
    ReturnLengthOfArg {
        arg: usize,
    },
    ReturnIsEmptyOfArg {
        arg: usize,
    },
    ReturnMin {
        lhs_arg: usize,
        rhs_arg: usize,
    },
    ReturnMax {
        lhs_arg: usize,
        rhs_arg: usize,
    },
    ReturnClamp {
        value_arg: usize,
        min_arg: usize,
        max_arg: usize,
    },
    ReturnAbs {
        arg: usize,
    },
    ReturnNeg {
        arg: usize,
    },
    ReturnAdd {
        lhs_arg: usize,
        rhs_arg: usize,
    },
    ReturnSub {
        lhs_arg: usize,
        rhs_arg: usize,
    },
    ReturnMul {
        lhs_arg: usize,
        rhs_arg: usize,
    },
    ReturnOptionSomeAdd {
        lhs_arg: usize,
        rhs_arg: usize,
    },
    ReturnOptionSomeMul {
        lhs_arg: usize,
        rhs_arg: usize,
    },
    ReturnNonZeroIff {
        arg: usize,
    },
    ReturnOptionSomeNonZeroIff {
        arg: usize,
    },
    ReturnTupleFieldNonZero {
        field: usize,
    },
    ReturnTupleFieldLength {
        field: usize,
        from_arg: usize,
    },
    ReturnNewAllocation {
        size_arg: usize,
        elem_size: u64,
    },
    ReturnNewAllocationFromBox {
        box_arg: usize,
    },
    ReturnAllocBuffer,
    ReturnPowerOfTwo,
    ReturnBoxFromVec {
        arg: usize,
    },
    OwnsInitMemory {
        arg: usize,
    },
    ChecksIndexBoundsDisjoint {
        indices_arg: usize,
        len_arg: usize,
    },
    ReturnOptionSomeScanIndex {
        self_arg: usize,
    },
    ReturnScanLength {
        ptr_arg: usize,
    },
    CleanSliceDataLinks {
        arg: usize,
    },
    ReturnOffsetFromUnsigned {
        self_arg: usize,
        origin_arg: usize,
    },
    ReturnAlignOffset {
        ptr_arg: usize,
        align_arg: usize,
    },
    ReturnAlignTo {
        receiver_arg: usize,
    },
    ReturnIter {
        receiver_arg: usize,
    },
    ReturnTransparentDeref {
        arg: usize,
        peel: usize,
    },
}

Path-local effect produced by a retained call.

Variants

ReturnAliasArg

The return value aliases or is a direct value flow from an argument.

Fields

arg: usize

ReturnPointerFromArg

The return value is a pointer extracted from an aggregate/reference arg.

Fields

arg: usize

ReturnPointerAdd

The return value is base + offset * stride.

Fields

base_arg: usize

offset_arg: usize

stride: Option<u64>

ReturnPointerSub

The return value is base - offset * stride.

Fields

base_arg: usize

offset_arg: usize

stride: Option<u64>

ReturnNonZero

The return value is known to be non-zero.

ReturnAligned

The return value is known to satisfy a concrete alignment.

Fields

align: u64

ty_name: String

ReturnConst

The return value is a concrete layout/numeric constant.

Fields

value: u64

label: String

ReadMemory

The call reads memory through an argument.

Fields

arg: usize

WriteMemory

The call writes one initialized element through a pointer argument.

Fields

pointer_arg: usize

ReturnFreshAllocation

The return value is a pointer backed by a fresh allocation of size_arg elements × elem_size bytes. The base address is taken from pointer_arg. Used for from_raw_parts(ptr, len).

Fields

pointer_arg: usize

size_arg: usize

elem_size: u64

ReturnLengthOfArg

The return value is the length of an aggregate argument.

Fields

arg: usize

ReturnIsEmptyOfArg

The return value is 1 iff the length of the aggregate argument is 0.

Fields

arg: usize

ReturnMin

The return value is min(lhs_arg, rhs_arg), satisfying return <= lhs_arg and return <= rhs_arg.

Fields

lhs_arg: usize

rhs_arg: usize

ReturnMax

The return value is max(lhs_arg, rhs_arg).

Fields

lhs_arg: usize

rhs_arg: usize

ReturnClamp

The return value is clamp(value_arg, min_arg, max_arg).

Fields

value_arg: usize

min_arg: usize

max_arg: usize

ReturnAbs

The return value is the absolute value of arg (ite(arg >= 0, arg, -arg)).

Fields

arg: usize

ReturnNeg

The return value is the negation of arg (-arg).

Fields

arg: usize

ReturnAdd

The return value is lhs_arg + rhs_arg.

Fields

lhs_arg: usize

rhs_arg: usize

ReturnSub

The return value is lhs_arg - rhs_arg.

Fields

lhs_arg: usize

rhs_arg: usize

ReturnMul

The return value is lhs_arg * rhs_arg.

Fields

lhs_arg: usize

rhs_arg: usize

ReturnOptionSomeAdd

The call returns Option<T> whose Some payload is lhs_arg + rhs_arg (models checked_add; the payload is non-zero whenever lhs_arg is).

Fields

lhs_arg: usize

rhs_arg: usize

ReturnOptionSomeMul

The call returns Option<T> whose Some payload is lhs_arg * rhs_arg (models checked_mul; the payload is non-zero whenever both args are).

Fields

lhs_arg: usize

rhs_arg: usize

ReturnNonZeroIff

The return value is non-zero iff arg is non-zero (models bit-preserving operations like rotate_left/swap_bytes/count_ones/isqrt, which map 0 to 0 and non-zero to non-zero).

Fields

arg: usize

ReturnOptionSomeNonZeroIff

The call returns Option<T> whose Some payload is non-zero iff arg is non-zero (models checked_pow).

Fields

arg: usize

ReturnTupleFieldNonZero

A specific field of the returned tuple is known to be non-zero (e.g. overflowing_abs/overflowing_neg return (result, overflow) where result != 0). Used to discharge a downstream ValidNum(result != 0).

Fields

field: usize

ReturnTupleFieldLength

A specific field of the returned tuple carries the length of a given argument (e.g. split_at(mid) returns (left, right) where left.len() == mid).

Fields

field: usize

from_arg: usize

ReturnNewAllocation

The return value is a pointer backed by a fresh heap allocation of size_arg elements × elem_size bytes. Unlike ReturnFreshAllocation this does not require a pointer argument — used for constructors like Vec::from_elem(init, count) that allocate fresh memory.

Fields

size_arg: usize

elem_size: u64

ReturnNewAllocationFromBox

Like ReturnNewAllocation but the length is carried by the argument itself (a Box fat pointer) rather than a separate count argument. Used for into_vec / box_assume_init_into_vec_unsafe.

Fields

box_arg: usize

ReturnAllocBuffer

Allocator::allocate(self, layout) / allocate_zeroed returns a Result<NonNull<[u8]>, AllocError>. Model the Ok variant as a fresh external (unbounded) allocation so downstream NonNull/Allocated checks auto-pass regardless of the symbolic layout.size(). The Result downcast (((result as Ok).0)) then propagates the provenance.

ReturnPowerOfTwo

The return value is a non-zero power of two (models Layout::align).

ReturnBoxFromVec

The call transfers a Vec’s backing allocation into a Box (e.g. Vec::into_boxed_slice). Looks up the current heap allocation from the allocation’s slice_data via the argument’s stack provenance.

Fields

arg: usize

OwnsInitMemory

The return value is known to own initialized memory of the type pointed to by the indicated argument (e.g. Box::from_raw(p) owns one initialized T element reached through p).

Fields

arg: usize

ChecksIndexBoundsDisjoint

The call validates that every element of the array argument indices_arg is < args[len_arg] and that the elements are pairwise distinct, returning Err otherwise. On the Ok continuation the caller may assume InBound(index_access(slice_of(len_arg), indices_arg)) and NonOverlap(indices_arg). (A trusted interprocedural summary, like the std-primitive summaries — the validator’s body is not re-proved here.)

Fields

indices_arg: usize

len_arg: usize

ReturnOptionSomeScanIndex

The call returns Option<usize> whose Some payload is a scan index into the iterator argument self_arg (models Iterator::position / Iterator::find): Some(i) satisfies 0 <= i < self.len() where self is the Iter/IterMut struct produced by into_iter/iter.

Fields

self_arg: usize

ReturnScanLength

The call returns the length of a nul-terminated string (models strlen): 0 <= len < isize::MAX, so len + 1 (the byte length with the terminator) fits in isize::MAX — discharging the from_raw_parts ValidNum(size_of(T)*(len+1) <= isize::MAX) bound.

Fields

ptr_arg: usize

CleanSliceDataLinks

Remove the allocation’s slice_data link for the argument’s stack alloc_id — used for mem::forget which prevents a drop cascade.

Fields

arg: usize

ReturnOffsetFromUnsigned

Returns the element-count distance between two pointers with common provenance: (self_arg.addr() - origin_arg.addr()) / sizeof(T). Models NonNull::offset_from_unsigned / offset_from.

Fields

self_arg: usize

origin_arg: usize

ReturnAlignOffset

ptr.align_offset(align) returns an offset such that (ptr + offset) % align == 0 and 0 <= offset < align (or usize::MAX when no such offset exists). Models *const T::align_offset / *mut T::align_offset by recording the alignment path-condition so downstream ptr.add(offset) dereferences can discharge Align.

Fields

ptr_arg: usize

align_arg: usize

ReturnAlignTo

A local align_to-style wrapper (align_to_ext/align_to_mut_ext) returns (prefix, body, suffix) where body is align_of::<U>()-aligned. Models the tuple by creating three sub-slices whose lengths/offsets obey prefix.len() = offset and len - suffix.len() = offset + k*size_of::<U>(), and records (ptr + offset) % align_of::<U>() == 0 so downstream ptr.add(offset - k) dereferences can discharge Align.

Fields

receiver_arg: usize

ReturnIter

IntoIterator::into_iter on &[T] / &mut [T] returns an Iter/IterMut whose ptr (field 0) and end_or_len (field 1) share the source slice’s allocation. Models the constructor by materializing those two pointer fields so downstream Iterator::next / len / is_empty can resolve the iterator’s provenance and element type.

Fields

receiver_arg: usize

ReturnTransparentDeref

<ManuallyDrop<T> as Deref>::deref / MaybeDangling::as_ref return a reference to the inner value at the same address (transparent wrappers). The return aliases arg (a &T pointing at arg’s pointee) and its pointee field values are the argument’s field values with the leading peel transparent field-0 hops stripped.

Fields

arg: usize

peel: usize

Trait Implementations

impl Clone for CallEffect

fn clone(&self) -> CallEffect

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CallEffect

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

Formats the value using the given formatter.