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

diff --git a/Test/codeexpr/CodeExpr1.bpl b/Test/codeexpr/CodeExpr1.bpl
index 4e8faf3f..98e97cdb 100644
--- a/Test/codeexpr/CodeExpr1.bpl
+++ b/Test/codeexpr/CodeExpr1.bpl
@@ -1,69 +1,69 @@
-// RUN: %boogie "%s" > "%t"

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

-// ------ the good ------

-

-procedure F(x: int, y: int) returns (z: bool)

-  requires x < y;

-  ensures z == (x < 3);

-{

-  start:

-    z := |{ var a : bool, b : bool; B: a := x < 3; return a; }|;

-    return;

-}

-

-function r(int): bool;

-

-procedure F'(x: int, y: int) returns (z: bool)

-{

-  start:

-    assume x < y;

-    assume (forall t: int :: x < 3 + t ==> r(t));

-    assert r(y);

-}

-

-procedure F''(x: int, y: int) returns (z: bool)

-{

-  start:

-    assume x < y;

-    assume (forall t: int :: |{ var a: bool;

-                                Start:

-                                a := x < 3 + t;

-                                goto X, Y;

-                                X: assume a; return r(t);

-                                Y: assume !a; return true;

-                             }|);

-    assert r(y);

-}

-

-// ------ the bad ------

-

-procedure G(x: int, y: int) returns (z: bool)

-  requires x < y;

-  ensures z == (x < 3);

-{

-  start:

-    z := |{ var a : bool, b : bool; B: a := x < 3; return !a; }|;

-    return;  // error: postcondition violation

-}

-

-procedure G'(x: int, y: int) returns (z: bool)

-{

-  start:

-    assume x < y;

-    assume (forall t: int :: x + 3 < t ==> r(t));

-    assert r(y);  // error

-}

-

-procedure G''(x: int, y: int) returns (z: bool)

-{

-  start:

-    assume x < y;

-    assume (forall t: int :: |{ var a: bool;

-                                Start:

-                                a := x + 3 < t;

-                                goto X, Y;

-                                X: assume a; return r(t);

-                                Y: assume !a; return true;

-                             }|);

-    assert r(y);  // error

-}

+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// ------ the good ------
+
+procedure F(x: int, y: int) returns (z: bool)
+  requires x < y;
+  ensures z == (x < 3);
+{
+  start:
+    z := |{ var a : bool, b : bool; B: a := x < 3; return a; }|;
+    return;
+}
+
+function r(int): bool;
+
+procedure F'(x: int, y: int) returns (z: bool)
+{
+  start:
+    assume x < y;
+    assume (forall t: int :: x < 3 + t ==> r(t));
+    assert r(y);
+}
+
+procedure F''(x: int, y: int) returns (z: bool)
+{
+  start:
+    assume x < y;
+    assume (forall t: int :: |{ var a: bool;
+                                Start:
+                                a := x < 3 + t;
+                                goto X, Y;
+                                X: assume a; return r(t);
+                                Y: assume !a; return true;
+                             }|);
+    assert r(y);
+}
+
+// ------ the bad ------
+
+procedure G(x: int, y: int) returns (z: bool)
+  requires x < y;
+  ensures z == (x < 3);
+{
+  start:
+    z := |{ var a : bool, b : bool; B: a := x < 3; return !a; }|;
+    return;  // error: postcondition violation
+}
+
+procedure G'(x: int, y: int) returns (z: bool)
+{
+  start:
+    assume x < y;
+    assume (forall t: int :: x + 3 < t ==> r(t));
+    assert r(y);  // error
+}
+
+procedure G''(x: int, y: int) returns (z: bool)
+{
+  start:
+    assume x < y;
+    assume (forall t: int :: |{ var a: bool;
+                                Start:
+                                a := x + 3 < t;
+                                goto X, Y;
+                                X: assume a; return r(t);
+                                Y: assume !a; return true;
+                             }|);
+    assert r(y);  // error
+}