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/Old.bpl | 268 ++++++++++++++++++++++++++---------------------------
 1 file changed, 134 insertions(+), 134 deletions(-)

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

diff --git a/Test/test2/Old.bpl b/Test/test2/Old.bpl
index beb98d40..017dcd85 100644
--- a/Test/test2/Old.bpl
+++ b/Test/test2/Old.bpl
@@ -1,134 +1,134 @@
-// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var x: int;
-var y: int;
-
-procedure P()
-  modifies x;
-  ensures x == old(x) + 1;
-{
-  start:
-    x := 1 + x;
-    return;
-}
-
-procedure Q();
-  modifies x;
-  ensures x == old(x) + 1;
-
-implementation Q()
-{
-  start:
-    x := 1 + x;
-    return;
-}
-
-procedure R()
-  modifies x;
-  ensures x == old(x) + 1;
-{
-  start:
-    return;
-}  // error: does not establish postcondition
-
-procedure Swap()
-  modifies x, y;
-  ensures x == old(y) && y == old(x);
-{
-  var t: int;
-
-  start:
-    goto A, B;
-  A:
-    t := x;
-    x := y;
-    y := t;
-    goto end;
-  B:
-    x := x - y;       // x == old(x) - old(y)
-    y := y + x;       // y == old(y) + (old(x) - old(y)) == old(x)
-    x := y - x;       // x == old(x) - (old(x) - old(y)) == old(y)
-    goto end;
-  end:
-    return;
-}
-
-procedure OutParam0(x: int) returns (y: int)
-  ensures y == x + 1;
-{
-  start:
-    y := x + 1;
-    return;
-}
-
-// OutParam1 is like OutParam0, except that there's now a separate
-// implementation declaration, which means that the specification
-// and body use different AST nodes for the formal parameters.  This
-// may make a difference in the various substitutions going on.
-// (Indeed, a previous bug caused OutParam0 to verify but not OutParam1.)
-procedure OutParam1(x: int) returns (y: int);
-  ensures y == x + 1;
-implementation OutParam1(x: int) returns (y: int)
-{
-  start:
-    y := x + 1;
-    return;
-}
-
-var a: [ref]int;
-var b: [ref]int;
-
-procedure SwapElems(o: ref) returns (p: ref)
-  modifies a, b;
-  ensures a[o] == old(b[p]) && b[o] == old(a[p]);
-{
-  var ta: int, tb: int;
-
-  start:
-    goto A, B, C;
-  A:
-    havoc p;
-    goto B, C;
-  B:
-    ta := a[p];
-    tb := b[p];
-    a[o] := tb;
-    b[o] := ta;
-    return;
-  C:
-    assume a[o] == b[o];assume false;
-
-    p := o;
-    return;
-}
-
-
-
-//-------------------------------------------------------------------------
-// Test old in Boogie PL code
-//-------------------------------------------------------------------------
-
-var Global0: int;
-
-// Good
-procedure OldInCode0()
-  requires Global0 >= 0;
-  ensures Global0 <= old(Global0) + 1;
-  modifies Global0;
-{
-  var local0: int;
- 
-  start:
-    goto A,B;
-  A:
-    assert Global0 == old(Global0);
-    return;
-
-  B:
-    local0 := Global0 + 1;
-    local0 := local0 - 1;
-    Global0 := old(local0 + 1);
-    return;
-}
-
-type ref;
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var x: int;
+var y: int;
+
+procedure P()
+  modifies x;
+  ensures x == old(x) + 1;
+{
+  start:
+    x := 1 + x;
+    return;
+}
+
+procedure Q();
+  modifies x;
+  ensures x == old(x) + 1;
+
+implementation Q()
+{
+  start:
+    x := 1 + x;
+    return;
+}
+
+procedure R()
+  modifies x;
+  ensures x == old(x) + 1;
+{
+  start:
+    return;
+}  // error: does not establish postcondition
+
+procedure Swap()
+  modifies x, y;
+  ensures x == old(y) && y == old(x);
+{
+  var t: int;
+
+  start:
+    goto A, B;
+  A:
+    t := x;
+    x := y;
+    y := t;
+    goto end;
+  B:
+    x := x - y;       // x == old(x) - old(y)
+    y := y + x;       // y == old(y) + (old(x) - old(y)) == old(x)
+    x := y - x;       // x == old(x) - (old(x) - old(y)) == old(y)
+    goto end;
+  end:
+    return;
+}
+
+procedure OutParam0(x: int) returns (y: int)
+  ensures y == x + 1;
+{
+  start:
+    y := x + 1;
+    return;
+}
+
+// OutParam1 is like OutParam0, except that there's now a separate
+// implementation declaration, which means that the specification
+// and body use different AST nodes for the formal parameters.  This
+// may make a difference in the various substitutions going on.
+// (Indeed, a previous bug caused OutParam0 to verify but not OutParam1.)
+procedure OutParam1(x: int) returns (y: int);
+  ensures y == x + 1;
+implementation OutParam1(x: int) returns (y: int)
+{
+  start:
+    y := x + 1;
+    return;
+}
+
+var a: [ref]int;
+var b: [ref]int;
+
+procedure SwapElems(o: ref) returns (p: ref)
+  modifies a, b;
+  ensures a[o] == old(b[p]) && b[o] == old(a[p]);
+{
+  var ta: int, tb: int;
+
+  start:
+    goto A, B, C;
+  A:
+    havoc p;
+    goto B, C;
+  B:
+    ta := a[p];
+    tb := b[p];
+    a[o] := tb;
+    b[o] := ta;
+    return;
+  C:
+    assume a[o] == b[o];assume false;
+
+    p := o;
+    return;
+}
+
+
+
+//-------------------------------------------------------------------------
+// Test old in Boogie PL code
+//-------------------------------------------------------------------------
+
+var Global0: int;
+
+// Good
+procedure OldInCode0()
+  requires Global0 >= 0;
+  ensures Global0 <= old(Global0) + 1;
+  modifies Global0;
+{
+  var local0: int;
+ 
+  start:
+    goto A,B;
+  A:
+    assert Global0 == old(Global0);
+    return;
+
+  B:
+    local0 := Global0 + 1;
+    local0 := local0 - 1;
+    Global0 := old(local0 + 1);
+    return;
+}
+
+type ref;
-- 
cgit v1.2.3