diff options
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 02d0f344..e6d05bea 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -633,6 +633,12 @@ procedure $IterHavoc1(this: ref, mod: Set BoxType, nw: Set BoxType); $o == this || mod[$Box($o)] || nw[$Box($o)]);
ensures $HeapSucc(old($Heap), $Heap);
+procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: ref, NW: Field (Set BoxType))
+ returns (s: Set BoxType);
+ ensures (forall bx: BoxType :: { s[bx] } s[bx] <==>
+ read(newHeap, this, NW)[bx] ||
+ ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc)));
+
// ---------------------------------------------------------------
// -- Non-determinism --------------------------------------------
// ---------------------------------------------------------------
|