summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-10-04 00:41:44 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2012-10-04 00:41:44 -0700
commit2d5a393b81ef2b389278f161460a1f98719c0aa6 (patch)
tree128e993567d6f392c11e3ab4f068da5f2a817db3 /Binaries
parent86da04e8be269d13874191c81cee0e2110d6373e (diff)
Dafny: fixed merge
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/DafnyPrelude.bpl12
1 files changed, 6 insertions, 6 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index fafc9484..342b72c1 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -615,22 +615,22 @@ procedure $YieldHavoc(this: ref, rds: Set BoxType, nw: Set BoxType);
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);
+// havoc everything in $Heap, except rds-modi-{this}
+procedure $IterHavoc0(this: ref, rds: Set BoxType, modi: 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 ==>
+ rds[$Box($o)] && !modi[$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);
+// havoc $Heap at {this}+modi+nw
+procedure $IterHavoc1(this: ref, modi: 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)]);
+ $o == this || modi[$Box($o)] || nw[$Box($o)]);
ensures $HeapSucc(old($Heap), $Heap);
procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: ref, NW: Field (Set BoxType))