Add leak check in Verification (at least for the debugger) #346
Description
Currently, emp is essentially true, meaning we don't catch memory leaks.
I forget if the leak check we have works in verification, or if it's just WPST.
We ought to:
- Make sure we have a working leak-check for verification
- Make sure this displays nicely in the debugger
- Should this be part of the match?
- Should we have an extra node for the leak check?
- Would this go at the end of the match, or the end of the function?
- Could this be made a special case of matching, to make sure the preds & heap are empty? This might require detectingn whether predicates are pure so they're not counted.