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

diff --git a/Test/test2/B.bpl b/Test/test2/B.bpl
index 78f91915..c90c156b 100644
--- a/Test/test2/B.bpl
+++ b/Test/test2/B.bpl
@@ -1,88 +1,88 @@
-// RUN: %boogie -noinfer "%s" > "%t"

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

-// ----------- BEGIN PRELUDE

-

-var Heap: [ref, name]int;

-const N: name;

-

-procedure Q0()

-{

-  var h: int;

-

-  entry:

-    goto Else;

-

-  Then:

-    h := 15;

-    goto end;

-

-  Else:

-    assume h == 0;

-    goto end;

-

-  end:

-    assert 0 <= h;

-    return;

-}

-

-procedure Q1()

-{

-  var h: int;

-

-  entry:

-    goto Else;

-

-  Then:

-    h := -15;

-    goto end;

-

-  Else:

-    assume h == 0;

-    goto end;

-

-  end:

-    h := -h;

-    assert 0 <= h;

-    return;

-}

-

-procedure P0(this: ref)

-  modifies Heap;

-{

-  entry:

-    goto Else;

-

-  Then:

-    Heap[this, N] := 15;

-    goto end;

-

-  Else:

-    assume Heap[this, N] == 0;

-    goto end;

-

-  end:

-    assert 0 <= Heap[this, N];

-    return;

-}

-

-procedure P1(this: ref)

-  modifies Heap;

-{

-  entry:

-    goto Else;

-

-  Then:

-    Heap[this, N] := -15;

-    goto end;

-

-  Else:

-    assume Heap[this, N] == 0;

-    goto end;

-

-  end:

-    Heap[this, N] := -Heap[this, N];

-    assert 0 <= Heap[this, N];

-    return;

-}

-

-type name, ref;

+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// ----------- BEGIN PRELUDE
+
+var Heap: [ref, name]int;
+const N: name;
+
+procedure Q0()
+{
+  var h: int;
+
+  entry:
+    goto Else;
+
+  Then:
+    h := 15;
+    goto end;
+
+  Else:
+    assume h == 0;
+    goto end;
+
+  end:
+    assert 0 <= h;
+    return;
+}
+
+procedure Q1()
+{
+  var h: int;
+
+  entry:
+    goto Else;
+
+  Then:
+    h := -15;
+    goto end;
+
+  Else:
+    assume h == 0;
+    goto end;
+
+  end:
+    h := -h;
+    assert 0 <= h;
+    return;
+}
+
+procedure P0(this: ref)
+  modifies Heap;
+{
+  entry:
+    goto Else;
+
+  Then:
+    Heap[this, N] := 15;
+    goto end;
+
+  Else:
+    assume Heap[this, N] == 0;
+    goto end;
+
+  end:
+    assert 0 <= Heap[this, N];
+    return;
+}
+
+procedure P1(this: ref)
+  modifies Heap;
+{
+  entry:
+    goto Else;
+
+  Then:
+    Heap[this, N] := -15;
+    goto end;
+
+  Else:
+    assume Heap[this, N] == 0;
+    goto end;
+
+  end:
+    Heap[this, N] := -Heap[this, N];
+    assert 0 <= Heap[this, N];
+    return;
+}
+
+type name, ref;