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/test1/Frame1.bpl | 198 +++++++++++++++++++++++++-------------------------
 1 file changed, 99 insertions(+), 99 deletions(-)

(limited to 'Test/test1/Frame1.bpl')

diff --git a/Test/test1/Frame1.bpl b/Test/test1/Frame1.bpl
index 2ec70270..5e637660 100644
--- a/Test/test1/Frame1.bpl
+++ b/Test/test1/Frame1.bpl
@@ -1,99 +1,99 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g0: int;
-var g1: int;
-
-var h0: [ref, name]int;
-var h1: [ref, name]int;
-
-const X: name;
-
-procedure P(a: ref, hh: [ref, name]int) returns (b: int, hout: [ref, name]any);
-  modifies h1, g0;
-
-implementation P(a: ref, hh: [ref, name]int)
-               returns (b: int, hout: [ref, name]any) {
-  start:
-    g0 := 5;
-    g1 := 6;  // error: g1 is not in modifies clause
-    a := null;  // error: in-parameters are not mutable 
-    b := 12;
-    goto next;
-  next:
-    havoc g0;
-    havoc g1;  // error: g1 is not in modifies clause
-    havoc a;  // error: in-parameters are not mutable
-    havoc b;
-    goto more;
-  more:
-    hh[a,X] := 101;  // error: in-parameter (hh) is not mutable
-    h0[a,X] := 102;  // error: h0 is not in modifies clause
-    h1[a,X] := 103;
-    hh := h0;  // error: in-parameter is not mutable
-    h0 := h1;  // error: h0 is not in modifies clause
-    h1 := hh;
-    havoc hh;  // error: in-parameter is not mutable
-    havoc h0;  // error: h0 is not in modifies clause
-    havoc h1;
-    return;
-}
-
-procedure PX();
-  modifies h1, g0;
-
-procedure PY()
-  modifies h1, g0;
-{
-  start:
-    call PX();
-    call PY();
-    return;
-}
-
-procedure PZ()
-  modifies h1;
-{
-  start:
-    call PX();  // error: PX has larger frame than PZ
-    return;
-}
-
-procedure Q() returns (x: int, y: int, h: [ref, name]int)
-{
-  start:
-    return;
-}
-
-procedure QCallerBad()
-{
-  start:
-    call g0, g1, h0 := Q();
-    return;
-}
-
-procedure QCallerGood()
-  modifies g0, h0;
-{
-  var t: int;
-
-  start:
-    call t, g0, h0 := Q();
-    return;
-}
-
-procedure MismatchedTypes(x: int);
-
-implementation MismatchedTypes(x: bool)  // error
-{
-  start:
-    return;
-}
-implementation MismatchedTypes(y: bool)  // error (this time with a different name for the formal)
-{
-  start:
-    return;
-}
-
-
-type ref, name, any;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var g0: int;
+var g1: int;
+
+var h0: [ref, name]int;
+var h1: [ref, name]int;
+
+const X: name;
+
+procedure P(a: ref, hh: [ref, name]int) returns (b: int, hout: [ref, name]any);
+  modifies h1, g0;
+
+implementation P(a: ref, hh: [ref, name]int)
+               returns (b: int, hout: [ref, name]any) {
+  start:
+    g0 := 5;
+    g1 := 6;  // error: g1 is not in modifies clause
+    a := null;  // error: in-parameters are not mutable 
+    b := 12;
+    goto next;
+  next:
+    havoc g0;
+    havoc g1;  // error: g1 is not in modifies clause
+    havoc a;  // error: in-parameters are not mutable
+    havoc b;
+    goto more;
+  more:
+    hh[a,X] := 101;  // error: in-parameter (hh) is not mutable
+    h0[a,X] := 102;  // error: h0 is not in modifies clause
+    h1[a,X] := 103;
+    hh := h0;  // error: in-parameter is not mutable
+    h0 := h1;  // error: h0 is not in modifies clause
+    h1 := hh;
+    havoc hh;  // error: in-parameter is not mutable
+    havoc h0;  // error: h0 is not in modifies clause
+    havoc h1;
+    return;
+}
+
+procedure PX();
+  modifies h1, g0;
+
+procedure PY()
+  modifies h1, g0;
+{
+  start:
+    call PX();
+    call PY();
+    return;
+}
+
+procedure PZ()
+  modifies h1;
+{
+  start:
+    call PX();  // error: PX has larger frame than PZ
+    return;
+}
+
+procedure Q() returns (x: int, y: int, h: [ref, name]int)
+{
+  start:
+    return;
+}
+
+procedure QCallerBad()
+{
+  start:
+    call g0, g1, h0 := Q();
+    return;
+}
+
+procedure QCallerGood()
+  modifies g0, h0;
+{
+  var t: int;
+
+  start:
+    call t, g0, h0 := Q();
+    return;
+}
+
+procedure MismatchedTypes(x: int);
+
+implementation MismatchedTypes(x: bool)  // error
+{
+  start:
+    return;
+}
+implementation MismatchedTypes(y: bool)  // error (this time with a different name for the formal)
+{
+  start:
+    return;
+}
+
+
+type ref, name, any;
+const null : ref;
-- 
cgit v1.2.3