Skip to content

Add a good failure state for allocation failure

Rodolphe Lepigre requested to merge intptr into master
  • Record in the state whether there has been an allocation failure.
  • Allocation failure as a new statement value.
  • Modification of the step relation to allow allocation failure to propagate to all threads.
  • Hide reasoning about allocation failure in a lifting lemma.
  • Actually add an "allocation failure" reduction step.
  • Fix adequacy.
Edited by Rodolphe Lepigre

Merge request reports