Module non_null 

SMT lowering for the NonNull safety property.

This module reduces:

NonNull(p)

to the common SMT obligation:

NonZero { place: p }

The common model asserts path-local facts such as reference-derived pointers and as_ptr results as non-zero assumptions, then asks whether the target can still be zero.

Functions

check 🔒

Check NonNull by lowering it to SmtObligation::NonZero.