diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-12 13:53:03 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-12 13:53:03 -0700 |
| commit | f2eb93519ffd02b775d427d2909cebd0690dc090 (patch) | |
| tree | 732a829e9b3d3bd5cd4a7ca303bc06163aedc639 /Binaries/DafnyPrelude.bpl | |
| parent | a63e68b3fe5d2245ad86767fde5f12717fb57f79 (diff) | |
Dafny: beefed up allocation axioms for boxes stored in fields
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -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 -----------------------------------------------------
|