From 2c063fd43db8c75c50f9e3191bafb6691d2d3b39 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 May 2020 09:59:00 +0200
Subject: [PATCH] note some design choices

---
 theories/heap_lang/lang.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index ee332ffbb..76e077e55 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -15,6 +15,13 @@ Noteworthy design choices:
   [b] are evaluated.  With left-to-right evaluation, that triple is basically
   useless unless the user let-expands [b].
 
+- Even after deallocating a location, the heap remembers that these locations
+  were previously allocated and makes sure they do not get reused. This is
+  necessary to ensure soundness of the [meta] feature provided by [gen_heap].
+  Also, unlike in langauges like C, allocated and deallocated "blocks" do not
+  have to match up: you can allocate a large array of locations and then
+  deallocate a hole out of it in the middle.
+
 - For prophecy variables, we annotate the reduction steps with an "observation"
   and tweak adequacy such that WP knows all future observations. There is
   another possible choice: Use non-deterministic choice when creating a prophecy
-- 
GitLab