diff options
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 5 |
1 files changed, 5 insertions, 0 deletions
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 -----------------------------------------------------
|