From 6489805cff9bc62d1933ca31a0307dbd43cd60e9 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 2 Oct 2012 14:17:15 -0700
Subject: Dafny: incomplete snapshot of verification of iterators

---
 Binaries/DafnyPrelude.bpl | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index ca526173..572a1e29 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -602,6 +602,19 @@ axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) }
 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 $Heap \ {this} \ S
+procedure {:inline} $YieldHavoc(this: ref, S: 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 ||
+              S[$Box($o)]);
+
 // ---------------------------------------------------------------
 // -- Non-determinism --------------------------------------------
 // ---------------------------------------------------------------
-- 
cgit v1.2.3