Module allocated 

SMT lowering for the Allocated safety property.

Allocated(p, T, n) means the whole n-element range starting at p belongs to a single live allocation object. The lowering is intentionally object-sensitive: adjacent stack locals do not form one larger allocation even when their addresses happen to be close.

Functions

check 🔒

Check Allocated by lowering it to a common allocation obligation.