Module non_overlap 

SMT lowering for the NonOverlap safety property.

NonOverlap(a, b) is mostly used by copy/swap-style unsafe APIs. The contract tells us which pointer arguments must be disjoint; the element count usually comes from the call itself, e.g. copy_nonoverlapping(src, dst, count).

Functions

assignment_source_for_local 🔒

check 🔒

Check NonOverlap by lowering two pointer ranges to a common SMT obligation.

resolve_callsite_copy 🔒

rvalue_source_place 🔒