From 4977e01decc2823eda691acea9bbbe7e537c14dc Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Tue, 12 Jun 2012 13:53:03 -0700
Subject: Dafny: beefed up allocation axioms for boxes stored in fields

---
 Binaries/DafnyPrelude.bpl | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 742fd4e4..fef8fe1f 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -558,6 +558,11 @@ axiom (forall x: int, h: HeapType ::
 axiom (forall r: ref, h: HeapType ::
   { GenericAlloc($Box(r), h) }
   $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h));
+// boxes in the heap
+axiom (forall r: ref, f: Field BoxType, h: HeapType ::
+  { GenericAlloc(read(h, r, f), h) }
+  $IsGoodHeap(h) && r != null && read(h, r, alloc) ==>
+  GenericAlloc(read(h, r, f), h));
 
 // ---------------------------------------------------------------
 // -- Arrays -----------------------------------------------------
-- 
cgit v1.2.3