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/AssumeEnsures.bpl | 142 +++++++++++++++++++++----------------------
 1 file changed, 71 insertions(+), 71 deletions(-)

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

diff --git a/Test/test2/AssumeEnsures.bpl b/Test/test2/AssumeEnsures.bpl
index 74789135..2c5ad6a2 100644
--- a/Test/test2/AssumeEnsures.bpl
+++ b/Test/test2/AssumeEnsures.bpl
@@ -1,71 +1,71 @@
-// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g: int;
-
-procedure Foo() returns ();
-    modifies g;
-    free ensures 0 <= g;
-
-implementation Foo() returns ()
-{
-    entry:
-        g := g + 1;
-        return;
-}
-
-procedure BarGood() returns ()
-    modifies g;
-{
-    entry:
-        call Foo();
-        assert 0 <= g;
-        return;
-}
-
-procedure BarBad() returns ()
-    modifies g;
-{
-    entry:
-        call Foo();
-        assert 0 < g;
-        return;
-}
-
-// ----- Free preconditions
-
-procedure Proc() returns ();
-    free requires g == 15;
-
-implementation Proc() returns ()
-{
-    entry:
-        assert g > 10;  // yes, this condition can be used here
-        return;
-}
-
-implementation Proc() returns ()
-{
-    entry:
-        assert g < 10;  // error
-        return;
-}
-
-procedure Caller0() returns ()
-{
-    entry:
-        call Proc();  // yes, legal, since the precondition is not checked
-        return;
-}
-
-procedure Caller1() returns ()
-{
-    entry:
-        call Proc();
-        assert g > 10;  // error, because:
-        // Free preconditions are ignored (that is, treated as "skip") for the caller.
-        // This is a BoogiePL design choice.  Another alternative would be to treat free
-        // preconditions as assume commands also on the caller side, either in the order
-        // that all preconditions are given, or before or after all the checked preconditions
-        // have been checked.
-        return;
-}
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var g: int;
+
+procedure Foo() returns ();
+    modifies g;
+    free ensures 0 <= g;
+
+implementation Foo() returns ()
+{
+    entry:
+        g := g + 1;
+        return;
+}
+
+procedure BarGood() returns ()
+    modifies g;
+{
+    entry:
+        call Foo();
+        assert 0 <= g;
+        return;
+}
+
+procedure BarBad() returns ()
+    modifies g;
+{
+    entry:
+        call Foo();
+        assert 0 < g;
+        return;
+}
+
+// ----- Free preconditions
+
+procedure Proc() returns ();
+    free requires g == 15;
+
+implementation Proc() returns ()
+{
+    entry:
+        assert g > 10;  // yes, this condition can be used here
+        return;
+}
+
+implementation Proc() returns ()
+{
+    entry:
+        assert g < 10;  // error
+        return;
+}
+
+procedure Caller0() returns ()
+{
+    entry:
+        call Proc();  // yes, legal, since the precondition is not checked
+        return;
+}
+
+procedure Caller1() returns ()
+{
+    entry:
+        call Proc();
+        assert g > 10;  // error, because:
+        // Free preconditions are ignored (that is, treated as "skip") for the caller.
+        // This is a BoogiePL design choice.  Another alternative would be to treat free
+        // preconditions as assume commands also on the caller side, either in the order
+        // that all preconditions are given, or before or after all the checked preconditions
+        // have been checked.
+        return;
+}
-- 
cgit v1.2.3