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

diff --git a/Test/codeexpr/CodeExpr2.bpl b/Test/codeexpr/CodeExpr2.bpl
index 9d8beed7..0edaa8f4 100644
--- a/Test/codeexpr/CodeExpr2.bpl
+++ b/Test/codeexpr/CodeExpr2.bpl
@@ -1,52 +1,52 @@
-// RUN: %boogie "%s" > "%t"

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

-type T;

-const zero: T;

-

-function IsProperIndex(i: int, size: int): bool;

-

-procedure P(a: [int]T, n: int)

-  requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);

-{

-  call Q(a, n);

-}

-

-procedure Q(a: [int]T, n: int)

-  requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);

-{

-  call P(a, n);

-}

-

-procedure A(a: [int]T, n: int)

-{

-  assert

-    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)

-    ==>

-    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);

-}

-

-procedure B(a: [int]T, n: int)

-{

-  assert

-    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)

-    ==>

-    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);

-}

-

-procedure C(a: [int]T, n: int)

-{

-  Start:

-    assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);

-    goto Next;

-  Next:

-    assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);

-}

-

-procedure D(a: [int]T, n: int)

-{

-  Start:

-    assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);

-    goto Next;

-  Next:

-    assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);

-}

+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type T;
+const zero: T;
+
+function IsProperIndex(i: int, size: int): bool;
+
+procedure P(a: [int]T, n: int)
+  requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+{
+  call Q(a, n);
+}
+
+procedure Q(a: [int]T, n: int)
+  requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+{
+  call P(a, n);
+}
+
+procedure A(a: [int]T, n: int)
+{
+  assert
+    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)
+    ==>
+    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure B(a: [int]T, n: int)
+{
+  assert
+    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)
+    ==>
+    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}
+
+procedure C(a: [int]T, n: int)
+{
+  Start:
+    assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+    goto Next;
+  Next:
+    assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure D(a: [int]T, n: int)
+{
+  Start:
+    assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+    goto Next;
+  Next:
+    assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}