Skip to content

Commit

Permalink
Patch up allocate / malloc proofs using Heap_in_bounds lemmas
Browse files Browse the repository at this point in the history 
that *will* optimistically be true once we patch it in MemoryModel.v.
  • Loading branch information
@Chobbes
Chobbes committed Jun 5, 2023
1 parent 6a0bfeb commit deb13f1
Showing 1 changed file with 113 additions and 92 deletions.
Loading

0 comments on commit deb13f1

Please sign in to comment.