Normalise line endings using a .gitattributes file. Unfortunately

this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.

1 files changed, 36 insertions, 36 deletions

diff --git a/Test/test2/ContractEvaluationOrder.bpl b/Test/test2/ContractEvaluationOrder.bpl
index 8719dcfa..4115c4b0 100644
--- a/Test/test2/ContractEvaluationOrder.bpl
+++ b/Test/test2/ContractEvaluationOrder.bpl
@@ -1,36 +1,36 @@
-// RUN: %boogie "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-procedure P() returns (x, y: int)

-  ensures x == y;  // ensured by the body

-  ensures x == 0;  // error: not ensured by the body

-  ensures y == 0;  // follows from the previous two ensures clauses (provided they are

-                   // indeed evaluated in this order, which they are supposed to be)

-{

-  x := y;

-}

-

-procedure Q() returns (x, y: int)

-{

-  x := y;

-

-  assert x == y;  // ensured by the body

-  assert x == 0;  // error: not ensured by the body

-  assert y == 0;  // follows from the previous two asserts (provided they are

-                  // indeed evaluated in this order, which they are supposed to be)

-}

-

-procedure R()

-{

-  var a, b: int;

-  a := b;

-  call S(a, b);

-}

-

-procedure S(x, y: int)

-                    // In the call from R:

-  requires x == y;  // ensured by the body of R

-  requires x == 0;  // error: not ensured by the body of R

-  requires y == 0;  // follows from the previous two requires clauses (provided they are

-                    // indeed evaluated in this order, which they are supposed to be)

-{

-}

+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure P() returns (x, y: int)
+  ensures x == y;  // ensured by the body
+  ensures x == 0;  // error: not ensured by the body
+  ensures y == 0;  // follows from the previous two ensures clauses (provided they are
+                   // indeed evaluated in this order, which they are supposed to be)
+{
+  x := y;
+}
+
+procedure Q() returns (x, y: int)
+{
+  x := y;
+
+  assert x == y;  // ensured by the body
+  assert x == 0;  // error: not ensured by the body
+  assert y == 0;  // follows from the previous two asserts (provided they are
+                  // indeed evaluated in this order, which they are supposed to be)
+}
+
+procedure R()
+{
+  var a, b: int;
+  a := b;
+  call S(a, b);
+}
+
+procedure S(x, y: int)
+                    // In the call from R:
+  requires x == y;  // ensured by the body of R
+  requires x == 0;  // error: not ensured by the body of R
+  requires y == 0;  // follows from the previous two requires clauses (provided they are
+                    // indeed evaluated in this order, which they are supposed to be)
+{
+}