1 files changed, 37 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 5530f8a7..fafc9484 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -603,6 +603,43 @@ axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }
   $HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));
 
 // ---------------------------------------------------------------
+// -- Useful macros ----------------------------------------------
+// ---------------------------------------------------------------
+
+// havoc everything in $Heap, except {this}+rds+nw
+procedure $YieldHavoc(this: ref, rds: Set BoxType, nw: Set BoxType);
+  modifies $Heap;
+  ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
+            $o != null && read(old($Heap), $o, alloc) ==>
+            $o == this || rds[$Box($o)] || nw[$Box($o)] ==>
+              read($Heap, $o, $f) == read(old($Heap), $o, $f));
+  ensures $HeapSucc(old($Heap), $Heap);
+
+// havoc everything in $Heap, except rds-mod-{this}
+procedure $IterHavoc0(this: ref, rds: Set BoxType, mod: Set BoxType);
+  modifies $Heap;
+  ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
+            $o != null && read(old($Heap), $o, alloc) ==>
+            rds[$Box($o)] && !mod[$Box($o)] && $o != this ==>
+              read($Heap, $o, $f) == read(old($Heap), $o, $f));
+  ensures $HeapSucc(old($Heap), $Heap);
+
+// havoc $Heap at {this}+mod+nw
+procedure $IterHavoc1(this: ref, mod: Set BoxType, nw: Set BoxType);
+  modifies $Heap;
+  ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
+            $o != null && read(old($Heap), $o, alloc) ==>
+              read($Heap, $o, $f) == read(old($Heap), $o, $f) ||
+              $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 --------------------------------------------
 // ---------------------------------------------------------------