Expand description
Checkers for memory-shape properties: Align, NonNull, Allocated,
Init, and Alive.
These consume the VM’s provenance/invariant facts (e.g. align_n,
in_bounds, non_null) with fast paths, falling back to SMT over
value.z3_term and allocation base/size.