Select a strategy:
Abduction Naive Naive Store Store with Frame Inference Store with Abduction
Select a precondition to posit:
Minimal Storelet Abstraction Alternate Storelet Abstraction Minimal Precondition Empty Store Abstraction Empty Heap Read Precondition from Source
Select a postcondition to check:
Empty Heap Read Postcondition from Source
Enter the code you'd like to verify: