From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 23:14:18 -0600
Subject: Merging complete.  Everything looks good *crosses fingers*

---
 Test/test2/NullaryMaps.bpl | 118 ++++++++++++++++++++++-----------------------
 1 file changed, 59 insertions(+), 59 deletions(-)

(limited to 'Test/test2/NullaryMaps.bpl')

diff --git a/Test/test2/NullaryMaps.bpl b/Test/test2/NullaryMaps.bpl
index a02f4594..142d18f2 100644
--- a/Test/test2/NullaryMaps.bpl
+++ b/Test/test2/NullaryMaps.bpl
@@ -1,59 +1,59 @@
-// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// aren't these cool!
-
-var m: []int;
-var p: <a>[]a;
-
-type ref;
-const null: ref;
-
-procedure P()
-  requires m[] == 5;
-  modifies m;
-  modifies p;
-  ensures m[] == 30;
-  ensures p[] == null;
-{
-  m[] := 12;
-  p[] := 12;
-  p[] := true;
-  assert p[] == m[];
-  assert p[];
-  m := m[:= 30];
-  p := p[:=null];
-}
-
-procedure Q()
-  modifies m;
-{
-  assert m[] == 5;  // error
-  m[] := 30;
-  assert m[] == 5;  // error
-}
-
-procedure R()
-  modifies p;
-{
-  assert p[] < 3;  // error
-}
-
-// ----
-
-type Field a;
-type HeapType = <a>[ref, Field a]a;
-const F0: Field int;
-const F1: Field bool;
-const alloc: Field bool;
-var Heap: HeapType;
-procedure FrameCondition(this: ref)
-  modifies Heap;
-  ensures (forall<a> o: ref, f: Field a ::
-    Heap[o,f] == old(Heap)[o,f] ||
-    !old(Heap)[o,alloc] ||
-    (o == this && f == F0) ||
-    (o == this && f == F1)
-    );
-{
-}
-
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// aren't these cool!
+
+var m: []int;
+var p: <a>[]a;
+
+type ref;
+const null: ref;
+
+procedure P()
+  requires m[] == 5;
+  modifies m;
+  modifies p;
+  ensures m[] == 30;
+  ensures p[] == null;
+{
+  m[] := 12;
+  p[] := 12;
+  p[] := true;
+  assert p[] == m[];
+  assert p[];
+  m := m[:= 30];
+  p := p[:=null];
+}
+
+procedure Q()
+  modifies m;
+{
+  assert m[] == 5;  // error
+  m[] := 30;
+  assert m[] == 5;  // error
+}
+
+procedure R()
+  modifies p;
+{
+  assert p[] < 3;  // error
+}
+
+// ----
+
+type Field a;
+type HeapType = <a>[ref, Field a]a;
+const F0: Field int;
+const F1: Field bool;
+const alloc: Field bool;
+var Heap: HeapType;
+procedure FrameCondition(this: ref)
+  modifies Heap;
+  ensures (forall<a> o: ref, f: Field a ::
+    Heap[o,f] == old(Heap)[o,f] ||
+    !old(Heap)[o,alloc] ||
+    (o == this && f == F0) ||
+    (o == this && f == F1)
+    );
+{
+}
+
-- 
cgit v1.2.3