Add deallocation operation to HeapLang
It would be great if HeapLang would also support deallocation, to enable reasoning about programs that perform explicit deallocation. To support the
meta mechanism we have to ensure that locations never get reused but that seems fine -- we do not have ptr-int-casts.
We do have ptr equality tests though. I am not sure if we are willing to demand that locations must not have been deallocated yet for them to be comparable -- that makes ptr equality a memory-dependent operation, which is quite the pain. Maybe it is okay to not be super realistic in this regard?