Module util 

Shared helpers for the property checkers.

Argument/place resolution (target_value, eval_contract_expr), the smt_check “negate and prove” primitive, and size/byte-width utilities used by every checker family.

Functions

local_param_operand 🔒

Resolve a callee Local(n) to the corresponding checkpoint operand, using the callee’s real argument count. Returns None when the checkpoint has no callee or n is not an argument local.

maybe_uninit_inner 🔒

Unwrap MaybeUninit<T> to T (or None for any other type). MaybeUninit is #[repr(transparent)] over a union, so MaybeUninit<T> and T share size and alignment.

smart_pointer_pointee 🔒

Peel one level of smart-pointer indirection to the pointee type: Box<T>/Vec<T>/NonNull<T>/Rc<T>/CString (matched by DefId), plus raw pointers and references. Used by check_allocated to discharge Allocated(p, Box<T>, n) after provenance resolution has already penetrated p (e.g. a &mut ManuallyDrop<Box<T>>) down to the T allocation: the box’s pointee is what actually occupies the allocation.