From 912adaa06621d89a47460d6a6befd8809ded5c85 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 20 Mar 2014 15:01:57 -0700
Subject: Fixed problem with propagating allocation information about array
 elements. Improved situation with (reducing bogosity of) type checking of
 "object".

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

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index ffc6715b..b6fce82c 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -662,6 +662,18 @@ axiom (forall r: ref, f: Field BoxType, h: HeapType ::
   $IsGoodHeap(h) && r != null && read(h, r, alloc) ==>
   GenericAlloc(read(h, r, f), h));
 
+axiom (forall h: HeapType, r: ref, j: int ::
+ { read(h, r, IndexField(j)) }
+ $IsGoodHeap(h) && r != null && read(h, r, alloc)
+ ==>
+ GenericAlloc(read(h, r, IndexField(j)), h));
+axiom (forall h: HeapType, r: ref, m: Field BoxType, j: int ::
+ { read(h, r, MultiIndexField(m, j)) }
+ $IsGoodHeap(h) && r != null && read(h, r, alloc)
+ ==>
+ GenericAlloc(read(h, r, MultiIndexField(m, j)), h));
+
+
 // ---------------------------------------------------------------
 // -- Arrays -----------------------------------------------------
 // ---------------------------------------------------------------
-- 
cgit v1.2.3