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, 64 insertions, 64 deletions

diff --git a/Test/test0/WhereResolution.bpl b/Test/test0/WhereResolution.bpl
index fac91dc8..9083d1fa 100644
--- a/Test/test0/WhereResolution.bpl
+++ b/Test/test0/WhereResolution.bpl
@@ -1,64 +1,64 @@
-// RUN: %boogie -noVerify "%s" > "%t"

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

-type double;

-

-function R(int) returns (bool);

-function K(double, bool) returns (bool);

-

-var y: int where R(y);

-var g: int where h ==> g == 12;

-var h: bool where g < 100;

-var k: double where K(k, h);

-

-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) returns (yy: int)

-{

-  var a: int where a == 10;

-  var b: int where a == b && b < g;

-

-  start:

-    a := xx;

-    call b := P(a);

-    yy := b;

-    return;

-}

-

-procedure Q(w: int where x < w || x > alpha/*error: out-parameter alpha is not in scope*/, x: int where x + w > 0)

-    returns (v: bool where v,

-             y: int where x + y + z < 0,

-             z: int where g == 12,

-             alpha: ref where old(alpha) != null,  // error: cannot use old in where clause

-             beta: ref where (forall r: ref :: r == beta ==> beta == null))

-  requires x < 100;

-  modifies g;

-  ensures -100 < y;

-{

-  var a: int;

-  var b: int;

-

-  start:

-    a := x;

-    call b := P(a);

-    y := b;

-    return;

-}

-

-const SomeConstant: ref;

-

-procedure Cnst(n: ref where n != SomeConstant) returns (SomeConstant: int)

-{

-  var m: ref where m != SomeConstant;

-  var k: int where k != SomeConstant;

-  var r: ref where (forall abc: ref :: abc == SomeConstant);

-  var b: bool;

-  start:

-    b := (forall l: ref :: l == SomeConstant);

-    return;

-}

-

-type ref;

-const null : ref;

+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type double;
+
+function R(int) returns (bool);
+function K(double, bool) returns (bool);
+
+var y: int where R(y);
+var g: int where h ==> g == 12;
+var h: bool where g < 100;
+var k: double where K(k, h);
+
+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) returns (yy: int)
+{
+  var a: int where a == 10;
+  var b: int where a == b && b < g;
+
+  start:
+    a := xx;
+    call b := P(a);
+    yy := b;
+    return;
+}
+
+procedure Q(w: int where x < w || x > alpha/*error: out-parameter alpha is not in scope*/, x: int where x + w > 0)
+    returns (v: bool where v,
+             y: int where x + y + z < 0,
+             z: int where g == 12,
+             alpha: ref where old(alpha) != null,  // error: cannot use old in where clause
+             beta: ref where (forall r: ref :: r == beta ==> beta == null))
+  requires x < 100;
+  modifies g;
+  ensures -100 < y;
+{
+  var a: int;
+  var b: int;
+
+  start:
+    a := x;
+    call b := P(a);
+    y := b;
+    return;
+}
+
+const SomeConstant: ref;
+
+procedure Cnst(n: ref where n != SomeConstant) returns (SomeConstant: int)
+{
+  var m: ref where m != SomeConstant;
+  var k: int where k != SomeConstant;
+  var r: ref where (forall abc: ref :: abc == SomeConstant);
+  var b: bool;
+  start:
+    b := (forall l: ref :: l == SomeConstant);
+    return;
+}
+
+type ref;
+const null : ref;