Module valid_ptr 

SMT lowering for the composite ValidPtr safety property.

ValidPtr(p, T, n) is not a primitive SMT obligation. The verifier reduces it to the pointer-validity formula used by the staged SMT checker:

ValidPtr(p, T, n) =
  Size(T, 0) || (!Size(T, 0) && Deref(p, T, n))

Deref(p, T, n) =
  Allocated(p, T, n, *) && InBound(p, T, n)

Zero-sized types do not require an allocated dereferenceable range. For non-ZSTs, ValidPtr delegates to the Deref composite checker.

Functions

check 🔒

Check ValidPtr using Size(T,0) || (!Size(T,0) && Deref(p,T,n)).

primitive_property 🔒

Reuse the original arguments while checking one primitive component.