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 | 4977e01decc2823eda691acea9bbbe7e537c14dc (patch) | |
| tree | 93461a8517756494f744ea4d094eed4e71989737 /Binaries | |
| parent | 84cd85ffd3c722278eb22d0bf402caf0f717a150 (diff) | |
Dafny: beefed up allocation axioms for boxes stored in fields
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 -----------------------------------------------------
|