Skip to main content

eff_ptr_arith

rapx::verify::call_summary::builtin_models

Function eff_ptr_arith 

Source 
fn eff_ptr_arith(
    ctx: &EffCtx<'_, '_>,
    dir: PtrDirection,
    granularity: PtrGranularity,
) -> Vec<CallEffect>
Expand description

Shared model for ReturnPointerAdd/ReturnPointerSub.

wrapping_add/wrapping_sub are shared between integers and raw pointers. When the destination is not a pointer type the call is an integer wrapping_add, whose result may wrap to zero, so it is left unconstrained rather than modelled as pointer arithmetic.