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/test0/WhereParsing.bpl b/Test/test0/WhereParsing.bpl
index e75a1c81..e6a0ab4e 100644
--- a/Test/test0/WhereParsing.bpl
+++ b/Test/test0/WhereParsing.bpl
@@ -1,36 +1,36 @@
-// RUN: %boogie -noVerify "%s" > "%t"

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

-const x: int;

-

-function R(int) returns (bool);

-function Even(int) returns (bool);

-

-var y: int where R(y);

-var g: int where g == 12;

-

-procedure P(x: int where x > 0) returns (y: int where y < 0);

-  requires x < 100;

-  modifies g;

-  ensures -100 < y;

-

-implementation P(xx: int where xx > 0)  // error: where not allowed in implementation decl

-    returns (yy: int where yy < 0)      // error: where not allowed in implementation decl

-{

-  var a: int where a == b;  // b is not allowed to be mentioned here, but this test is only

-  var b: int;               // for parsing, so no complaint will be issued

-

-  start:

-    a := xx;

-    call b := P(a);

-    yy := b;

-    return;

-}

-

-procedure {:myProcAttr} Attr(x: int, {:myParamAttr x, y} y: bool) returns (z: int, {:retAttr x} w: bool)

-{

-}

-

-procedure BadAttrs(x: int);

-implementation BadAttrs({:myParamAttr} x: int)  // error: attributes not allowed in implementation decl

-{

-}

+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+const x: int;
+
+function R(int) returns (bool);
+function Even(int) returns (bool);
+
+var y: int where R(y);
+var g: int where g == 12;
+
+procedure P(x: int where x > 0) returns (y: int where y < 0);
+  requires x < 100;
+  modifies g;
+  ensures -100 < y;
+
+implementation P(xx: int where xx > 0)  // error: where not allowed in implementation decl
+    returns (yy: int where yy < 0)      // error: where not allowed in implementation decl
+{
+  var a: int where a == b;  // b is not allowed to be mentioned here, but this test is only
+  var b: int;               // for parsing, so no complaint will be issued
+
+  start:
+    a := xx;
+    call b := P(a);
+    yy := b;
+    return;
+}
+
+procedure {:myProcAttr} Attr(x: int, {:myParamAttr x, y} y: bool) returns (z: int, {:retAttr x} w: bool)
+{
+}
+
+procedure BadAttrs(x: int);
+implementation BadAttrs({:myParamAttr} x: int)  // error: attributes not allowed in implementation decl
+{
+}