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

diff --git a/Test/test0/Arrays1.bpl b/Test/test0/Arrays1.bpl
index 4e031cb8..0c9f6044 100644
--- a/Test/test0/Arrays1.bpl
+++ b/Test/test0/Arrays1.bpl
@@ -1,22 +1,22 @@
-// RUN: %boogie -noVerify "%s" | %OutputCheck "%s"

-var Q: [int,int][int]int;

-

-procedure P()

-{

-  var q: [int]int;

-

-  start:

-    // here's how to do it:

-    q := Q[5,8];

-    q[13] := 21;

-

-    // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q

-    Q[5,8] := q;

-

-    // not like this:

-    // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q

-    Q[5,8][13] := 21;  // error: the updated array must be an identifier

-    return;

-}

-

-// CHECK-L: 2 type checking errors detected in ${CHECKFILE_NAME}

+// RUN: %boogie -noVerify "%s" | %OutputCheck "%s"
+var Q: [int,int][int]int;
+
+procedure P()
+{
+  var q: [int]int;
+
+  start:
+    // here's how to do it:
+    q := Q[5,8];
+    q[13] := 21;
+
+    // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+    Q[5,8] := q;
+
+    // not like this:
+    // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+    Q[5,8][13] := 21;  // error: the updated array must be an identifier
+    return;
+}
+
+// CHECK-L: 2 type checking errors detected in ${CHECKFILE_NAME}