Enum CallEffect 

pub(crate) enum CallEffect {
    ReturnAliasArg {
        arg: usize,
    },
    SelectUnpredictable,
    ReturnPointerFromArg {
        arg: usize,
    },
    ReturnPointerAdd {
        base_arg: usize,
        offset_arg: usize,
        stride: Option<u64>,
        dereferenceable: bool,
    },
    ReturnPointerSub {
        base_arg: usize,
        offset_arg: usize,
        stride: Option<u64>,
    },
    ReturnNonZero,
    ReturnAligned,
    ReturnConst {
        value: u64,
    },
    WriteMemory {
        pointer_arg: usize,
    },
    ReturnFreshAllocation {
        pointer_arg: usize,
        size_arg: usize,
        elem_size: u64,
    },
    ReturnExchangeMalloc {
        size_arg: usize,
    },
    ReturnLengthOfArg {
        arg: usize,
    },
    ReturnFieldOfArg {
        arg: usize,
        field: usize,
    },
    ReturnFieldOfArgSub {
        arg: usize,
        field: usize,
        offset: u64,
    },
    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,
    },
    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,
    },
    ReturnOptionSomeNonZero,
    ReturnTupleFieldNonZero {
        field: usize,
    },
    ReturnTupleFieldLength {
        field: usize,
        from_arg: usize,
    },
    ReturnNewAllocation {
        size_arg: usize,
        elem_size: u64,
    },
    ReturnBoxAllocation,
    ReturnNewAllocationFromBox,
    ReturnNewAllocationFromCap {
        cap_arg: usize,
        elem_size: u64,
    },
    ReturnPowerOfTwo,
    ReturnBoxFromVec {
        arg: usize,
    },
    OwnsInitMemory {
        arg: usize,
    },
    ChecksIndexBoundsDisjoint {
        indices_arg: usize,
        len_arg: usize,
    },
    ReturnOptionSomeScanIndex {
        self_arg: usize,
    },
    ReturnOptionSomeIndexLtArgLen {
        arg: usize,
    },
    ReturnOptionSomeTupleFieldLeArgLen {
        field: usize,
        arg: usize,
    },
    ReturnBranchPayload {
        arg: usize,
    },
    ReturnScanLength,
    ReturnAlignOffset {
        ptr_arg: usize,
        align_arg: usize,
    },
    ReturnAlignTo {
        receiver_arg: usize,
    },
    ReturnIter {
        receiver_arg: usize,
    },
    ReturnTransparentDeref {
        arg: usize,
        peel: usize,
    },
    ReturnRange {
        bounds_arg: usize,
    },
    ReturnDerefArg {
        arg: usize,
    },
    DropMemory {
        pointer_arg: 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

SelectUnpredictable

select_unpredictable(cond, x, y) returns either x or y: the result is one of the two candidate values (args[1]/args[2]), non-deterministic since the boolean selector (args[0]) is unpredictable.

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>

dereferenceable: bool

Whether the result is a dereferenceable pointer (its contract guarantees strict in-bounds, e.g. SliceIndex::get_unchecked), as opposed to plain add arithmetic whose result may be one-past-end.

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.

ReturnConst

The return value is a concrete layout/numeric constant.

Fields

value: u64

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

ReturnExchangeMalloc

alloc::alloc::exchange_malloc(size, align) — a fresh allocation of size_arg bytes, returned as *mut u8.

Fields

size_arg: usize

ReturnLengthOfArg

The return value is the length of an aggregate argument.

Fields

arg: usize

ReturnFieldOfArg

The return value is field field of the pointee of argument arg (models Vec::len and any (*self).field getter; the field index is derived straight from the callee’s MIR).

Fields

arg: usize

field: usize

ReturnFieldOfArgSub

The return value is field field of the pointee of argument arg, minus offset elements. Models an iterator’s next_back_unchecked, which mutates its end_or_len field via pre_dec_end(offset) before returning it — so the returned pointer is field - offset elements past the stored field value.

Fields

arg: usize

field: usize

offset: u64

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

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

ReturnOptionSomeNonZero

The call returns Option<T> whose Some payload is unconditionally non-zero (models checked_next_power_of_two, where the next power of two is always positive regardless of the argument).

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

ReturnBoxAllocation

Box::new / Box::new_in / Box::new_uninit / Box::new_uninit_in (and try_ variants): allocate a fresh heap buffer of size_of::<T>() bytes and return a Box whose pointer field backs it. These have MIR available but carry a match on the allocator’s Result, which the inline heuristic rejects as a semantic branch, so a direct effect is the only way the fresh allocation’s provenance reaches the NonNull.

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.

ReturnNewAllocationFromCap

Like ReturnNewAllocation, but the argument is the capacity: the returned Vec starts empty (len == 0) with cap == cap_arg (models Vec::with_capacity).

Fields

cap_arg: usize

elem_size: u64

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 argument’s owning pointer field via its 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(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

ReturnOptionSomeIndexLtArgLen

The call returns Option<usize> whose Some payload i is an index into the slice argument arg: i < args[arg].len(). Detected from the callee’s MIR shape (while i < arg.len() { ... return Some(i); ... }, i.e. memchr-style search). Lets a caller re-prove a numeric invariant like finger <= finger_back after finger += i + 1.

Fields

arg: usize

ReturnOptionSomeTupleFieldLeArgLen

The call returns Option<(.., usize, ..)> whose tuple field field (a byte length) is <= args[arg].len(). Detected from a UTF-8-decoder shape: each Some((.., len)) return is guarded by slice.get(len - 1)?.

Fields

field: usize

arg: usize

ReturnBranchPayload

The call is Try::branch: Option<T> -> ControlFlow<Option<!>, T>, so the result’s Continue payload (field 0) equals the input’s Some payload (field 0). Models the ? operator’s if let Some(..) = expr? unwrap so the payload’s provenance survives the branch.

Fields

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.

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

ReturnRange

slice::range(range, bounds) returns Range { start, end } satisfying 0 <= start <= end <= bounds.end. Models the range normalizer whose start_bound/end_bound trait dispatch cannot be inlined.

Fields

bounds_arg: usize

ReturnDerefArg

mem::replace(dest, src) returns *dest (the old value), so the return is the pointee of the reference argument, not the reference itself.

Fields

arg: usize

DropMemory

The call frees the heap allocation behind pointer_arg (a &mut reference to a Box/Vec/String pointee). Models ManuallyDrop::drop.

Fields

pointer_arg: usize

Trait Implementations

impl Clone for CallEffect

fn clone(&self) -> Self

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.