From deb7703ccac449f9d7d560a465998d5d92cc92ae Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 12 May 2020 19:33:55 +0200 Subject: [PATCH] CHANGELOG, update gen_inv_heap comment --- CHANGELOG.md | 3 ++- theories/base_logic/lib/gen_inv_heap.v | 9 ++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c15d3c9c2..eadb54038 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -23,8 +23,9 @@ Coq development, but not every API-breaking change is listed. Changes marked **Changes in heap_lang:** +* Added support for deallocation of locations. * Added a fraction to the heap_lang `array` assertion. -* Added array_copy library for copying and cloning arrays. +* Added array_tools library for deallocating, copying and cloning arrays. * Added the ghost state for "invariant locations" to `heapG`. This affects the statement of `heap_adequacy`, which is now responsible for initializing the "invariant locations" invariant. diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v index 20311ce97..2f2de4cad 100644 --- a/theories/base_logic/lib/gen_inv_heap.v +++ b/theories/base_logic/lib/gen_inv_heap.v @@ -14,11 +14,10 @@ it is that they are reading in that case. In that extreme case, the invariant may just be [True]. Since invariant locations cannot be deallocated, they only make sense when -modelling languages with garbage collection. Note that heap_lang does not -actually have explicit dealloaction. However, the proof rules we provide for -heap operations currently are conservative in the sense that they do not expose -this fact. By making "invariant" locations a separate assertion, we can keep -all the other proofs that do not need it conservative. *) +modelling languages with garbage collection. HeapLang can be used to model +either language by choosing whether or not to use the [Free] operation. By +making "invariant" locations a separate assertion, we can keep all the other +proofs that do not need it conservative. *) Definition inv_heapN: namespace := nroot .@ "inv_heap". Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope. -- GitLab