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.

12 files changed, 216 insertions, 216 deletions

diff --git a/Test/bitvectors/arrays.bpl b/Test/bitvectors/arrays.bpl
index dae54e63..c6368fbe 100644
--- a/Test/bitvectors/arrays.bpl
+++ b/Test/bitvectors/arrays.bpl
@@ -1,43 +1,43 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

-const unique f1 : Field int;

-const unique f2 : Field bv32;

-const unique f3 : Field bool;

-

-const unique r1 : ref;

-const unique r2 : ref;

-

-var H : <x>[ref,Field x]x;

-

-procedure foo()

-  modifies H;

-{

-  var i : int;

-  var b : bv32;

-  var c : bool;

-

-  H[r1, f1] := 3;

-  H[r1, f2] := 77bv32;

-  H[r1, f3] := true;

-  i := H[r1,f1];

-  b := H[r1,f2];

-  c := H[r1,f3];

-  assert i == 3;

-  assert b == 77bv32;

-  assert H[r1,f3];

-}

-

-var B : [bv32]bv32;

-

-procedure bar()

-  modifies B;

-{

-  var b : bv32;

-

-  B[42bv32] := 77bv32;

-  b := B[42bv32];

-  assert b == 77bv32;

-}

-

-

+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+const unique f1 : Field int;
+const unique f2 : Field bv32;
+const unique f3 : Field bool;
+
+const unique r1 : ref;
+const unique r2 : ref;
+
+var H : <x>[ref,Field x]x;
+
+procedure foo()
+  modifies H;
+{
+  var i : int;
+  var b : bv32;
+  var c : bool;
+
+  H[r1, f1] := 3;
+  H[r1, f2] := 77bv32;
+  H[r1, f3] := true;
+  i := H[r1,f1];
+  b := H[r1,f2];
+  c := H[r1,f3];
+  assert i == 3;
+  assert b == 77bv32;
+  assert H[r1,f3];
+}
+
+var B : [bv32]bv32;
+
+procedure bar()
+  modifies B;
+{
+  var b : bv32;
+
+  B[42bv32] := 77bv32;
+  b := B[42bv32];
+  assert b == 77bv32;
+}
+
+
 type Field a, ref;
\ No newline at end of file
diff --git a/Test/bitvectors/bv0.bpl b/Test/bitvectors/bv0.bpl
index 8c330eda..d5a34bf5 100644
--- a/Test/bitvectors/bv0.bpl
+++ b/Test/bitvectors/bv0.bpl
@@ -1,15 +1,15 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

-procedure foo2(x : bv32) returns(r : bv32)

-{

-  block1:

-  	r := 17bv31; // Error

-  	r := 17; // Error

-    r := x[1:0]; // Error

-    r := x[0:1]; // Error

-    r := x[55:54]; // Error

-    r := x[33:32]; // Error

-    r := 17bv10 ++ 17bv42 ++ 13bv22; // Error

-    return;

-}

-

+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo2(x : bv32) returns(r : bv32)
+{
+  block1:
+  	r := 17bv31; // Error
+  	r := 17; // Error
+    r := x[1:0]; // Error
+    r := x[0:1]; // Error
+    r := x[55:54]; // Error
+    r := x[33:32]; // Error
+    r := 17bv10 ++ 17bv42 ++ 13bv22; // Error
+    return;
+}
+
diff --git a/Test/bitvectors/bv1.bpl b/Test/bitvectors/bv1.bpl
index 2edc5037..7a86bff7 100644
--- a/Test/bitvectors/bv1.bpl
+++ b/Test/bitvectors/bv1.bpl
@@ -1,19 +1,19 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

-procedure foo(x : bv32) returns(r : bv32)

-{

-  var q : bv64;

-

-  block1:

-  	r := 17bv32;

-	assert r == r;

-    assert r[32:0] == r[32:0];

-    assert 0bv2 ++ r[12:0] == 0bv2 ++ r[12:0];

-    r := 17bv10 ++ 17bv22;

-  	// r := 17;

-    q := 420000000000bv64;

-    q := 8444249301319680000bv64;

-    q := 16444249301319680000bv64;

-  return;

-}

-

+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(x : bv32) returns(r : bv32)
+{
+  var q : bv64;
+
+  block1:
+  	r := 17bv32;
+	assert r == r;
+    assert r[32:0] == r[32:0];
+    assert 0bv2 ++ r[12:0] == 0bv2 ++ r[12:0];
+    r := 17bv10 ++ 17bv22;
+  	// r := 17;
+    q := 420000000000bv64;
+    q := 8444249301319680000bv64;
+    q := 16444249301319680000bv64;
+  return;
+}
+
diff --git a/Test/bitvectors/bv10.bpl b/Test/bitvectors/bv10.bpl
index cacf9f7a..6ba4ad7a 100644
--- a/Test/bitvectors/bv10.bpl
+++ b/Test/bitvectors/bv10.bpl
@@ -1,12 +1,12 @@
-// RUN: %boogie "%s" > "%t"

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

-var x: bv32;

-

-procedure main() 

-modifies x;

-{

-

-  x := 0bv32;

-  assume x == 1bv32;

-  assert false;

-}

+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var x: bv32;
+
+procedure main() 
+modifies x;
+{
+
+  x := 0bv32;
+  assume x == 1bv32;
+  assert false;
+}
diff --git a/Test/bitvectors/bv2.bpl b/Test/bitvectors/bv2.bpl
index 45fdf7e4..8e2c1dad 100644
--- a/Test/bitvectors/bv2.bpl
+++ b/Test/bitvectors/bv2.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

-procedure foo2(x : bv32) returns(r : bv32)

-{

-  block1:

-    r := x[-1:1];  // Error

-//    r := x[x:1];  // Error

-    r := x[1:x];  // Error

-    r := x[1+1:3];  // Error

-    return;

-}

-

-

+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo2(x : bv32) returns(r : bv32)
+{
+  block1:
+    r := x[-1:1];  // Error
+//    r := x[x:1];  // Error
+    r := x[1:x];  // Error
+    r := x[1+1:3];  // Error
+    return;
+}
+
+
diff --git a/Test/bitvectors/bv3.bpl b/Test/bitvectors/bv3.bpl
index 5a2ce47f..5b21ca59 100644
--- a/Test/bitvectors/bv3.bpl
+++ b/Test/bitvectors/bv3.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

-type bv;

-type bv16;

-

+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type bv;
+type bv16;
+
diff --git a/Test/bitvectors/bv4.bpl b/Test/bitvectors/bv4.bpl
index 29c8130a..1e7b6e31 100644
--- a/Test/bitvectors/bv4.bpl
+++ b/Test/bitvectors/bv4.bpl
@@ -1,25 +1,25 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

-

-function a() returns(bv32);

-axiom a() == a();

-

-axiom 0bv5 != 1bv5;

-

-

-// -------------------------

-type $x;

-function g() returns($x);

-type Field x;

-var $gmem : <x>[ref, Field x] x;

-const unique f : Field $x;

-

-procedure qq()

-  modifies $gmem;

-{ 

-   $gmem[null, f] := g();

-}

-

-

-type ref;

-const null : ref;

+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function a() returns(bv32);
+axiom a() == a();
+
+axiom 0bv5 != 1bv5;
+
+
+// -------------------------
+type $x;
+function g() returns($x);
+type Field x;
+var $gmem : <x>[ref, Field x] x;
+const unique f : Field $x;
+
+procedure qq()
+  modifies $gmem;
+{ 
+   $gmem[null, f] := g();
+}
+
+
+type ref;
+const null : ref;
diff --git a/Test/bitvectors/bv5.bpl b/Test/bitvectors/bv5.bpl
index 73dff1ad..048bc315 100644
--- a/Test/bitvectors/bv5.bpl
+++ b/Test/bitvectors/bv5.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie  "%s" > "%t"

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

-

-procedure P() returns () {

-  var m : <a>[a]int;

-

-  m[23bv5] := 17;

-  m[21bv5] := 19;

-  m[21bv6] := -3;

-

-  assert m[23bv5] == 17;

-  assert m[21bv6] == 3; // should not be provable

-}

+// RUN: %boogie  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure P() returns () {
+  var m : <a>[a]int;
+
+  m[23bv5] := 17;
+  m[21bv5] := 19;
+  m[21bv6] := -3;
+
+  assert m[23bv5] == 17;
+  assert m[21bv6] == 3; // should not be provable
+}
diff --git a/Test/bitvectors/bv6.bpl b/Test/bitvectors/bv6.bpl
index d0654b6f..7ff4777f 100644
--- a/Test/bitvectors/bv6.bpl
+++ b/Test/bitvectors/bv6.bpl
@@ -1,11 +1,11 @@
-// RUN: %boogie  "%s" > "%t"

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

-

-procedure Q() returns () {

-  var x : bv32, y : bv16;

-

-  x := y ++ y;

-  assert x[16:0] == y;

-  assert x == x[16:0] ++ y;

-  assert x[17:1] == y;     // should not be verifiable

-}

+// RUN: %boogie  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure Q() returns () {
+  var x : bv32, y : bv16;
+
+  x := y ++ y;
+  assert x[16:0] == y;
+  assert x == x[16:0] ++ y;
+  assert x[17:1] == y;     // should not be verifiable
+}
diff --git a/Test/bitvectors/bv7.bpl b/Test/bitvectors/bv7.bpl
index a60f9547..5d32dda4 100644
--- a/Test/bitvectors/bv7.bpl
+++ b/Test/bitvectors/bv7.bpl
@@ -1,11 +1,11 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

-procedure foo2(x : bv32) returns(r : bv32)

-{

-  block1:

-    r := x[x:1];  // Error

-    r := x[(1:13)];  // Error

-    return;

-}

-

-

+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo2(x : bv32) returns(r : bv32)
+{
+  block1:
+    r := x[x:1];  // Error
+    r := x[(1:13)];  // Error
+    return;
+}
+
+
diff --git a/Test/bitvectors/bv8.bpl b/Test/bitvectors/bv8.bpl
index ee572998..557eb4e8 100644
--- a/Test/bitvectors/bv8.bpl
+++ b/Test/bitvectors/bv8.bpl
@@ -1,25 +1,25 @@
-// RUN: %boogie "%s" > "%t"

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

-// This file includes some tests for which Boogie once generated bad Z3 input

-

-procedure foo()

-{

-  var r: bv3;

-  var s: bv6;

-  var u: bv15;

-  var t: bv24;

-

-  t := t[8: 0] ++ t[10: 0] ++ t[24: 18];

-  t := (r ++ s) ++ u;

-  t := t[16: 0] ++ t[8: 0];

-}

-

-procedure bar()

-{

-  var a: bv64;

-  var b: bv32;

-  var c: bv8;

-

-  c := a[8:0];

-  c := b[8:0];

-}

+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// This file includes some tests for which Boogie once generated bad Z3 input
+
+procedure foo()
+{
+  var r: bv3;
+  var s: bv6;
+  var u: bv15;
+  var t: bv24;
+
+  t := t[8: 0] ++ t[10: 0] ++ t[24: 18];
+  t := (r ++ s) ++ u;
+  t := t[16: 0] ++ t[8: 0];
+}
+
+procedure bar()
+{
+  var a: bv64;
+  var b: bv32;
+  var c: bv8;
+
+  c := a[8:0];
+  c := b[8:0];
+}
diff --git a/Test/bitvectors/bv9.bpl b/Test/bitvectors/bv9.bpl
index 19a147ad..11c5156b 100644
--- a/Test/bitvectors/bv9.bpl
+++ b/Test/bitvectors/bv9.bpl
@@ -1,25 +1,25 @@
-// RUN: %boogie -proverOpt:OPTIMIZE_FOR_BV=true "%s" > "%t"

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

-procedure foo();

-

-implementation foo()

-{

-    assert (forall Q#a$1^15.32#tc1: bv64, Q#b$1^15.32#tc1: bv64, Q#c$1^15.32#tc1: bv64 :: true && true && true ==> ($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) == Q#c$1^15.32#tc1 || $bv_bvadd64($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), 1bv64) == Q#c$1^15.32#tc1) && (if Q#c$1^15.32#tc1 == $bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) then $bv_bvugt64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1)) else $bv_bvuge64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1))) ==> $bv_bvlshr64($bv_bvxor64($bv_bvor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), $bv_bvand64($bv_bvxor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), Q#c$1^15.32#tc1)), 0bv32 ++ 63bv32) == 1bv64);

-}

-

-function {:bvbuiltin "bvlshr"} $bv_bvlshr64(p1: bv64, p2: bv64) : bv64;

-

-function {:bvbuiltin "bvand"} $bv_bvand64(p1: bv64, p2: bv64) : bv64;

-

-function {:bvbuiltin "bvor"} $bv_bvor64(p1: bv64, p2: bv64) : bv64;

-

-function {:bvbuiltin "bvxor"} $bv_bvxor64(p1: bv64, p2: bv64) : bv64;

-

-function {:bvbuiltin "bvuge"} $bv_bvuge64(p1: bv64, p2: bv64) : bool;

-

-function {:bvbuiltin "bvugt"} $bv_bvugt64(p1: bv64, p2: bv64) : bool;

-

-function {:bvbuiltin "bvsub"} $bv_bvsub64(p1: bv64, p2: bv64) : bv64;

-

-function {:bvbuiltin "bvadd"} $bv_bvadd64(p1: bv64, p2: bv64) : bv64;

-

+// RUN: %boogie -proverOpt:OPTIMIZE_FOR_BV=true "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo();
+
+implementation foo()
+{
+    assert (forall Q#a$1^15.32#tc1: bv64, Q#b$1^15.32#tc1: bv64, Q#c$1^15.32#tc1: bv64 :: true && true && true ==> ($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) == Q#c$1^15.32#tc1 || $bv_bvadd64($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), 1bv64) == Q#c$1^15.32#tc1) && (if Q#c$1^15.32#tc1 == $bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) then $bv_bvugt64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1)) else $bv_bvuge64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1))) ==> $bv_bvlshr64($bv_bvxor64($bv_bvor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), $bv_bvand64($bv_bvxor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), Q#c$1^15.32#tc1)), 0bv32 ++ 63bv32) == 1bv64);
+}
+
+function {:bvbuiltin "bvlshr"} $bv_bvlshr64(p1: bv64, p2: bv64) : bv64;
+
+function {:bvbuiltin "bvand"} $bv_bvand64(p1: bv64, p2: bv64) : bv64;
+
+function {:bvbuiltin "bvor"} $bv_bvor64(p1: bv64, p2: bv64) : bv64;
+
+function {:bvbuiltin "bvxor"} $bv_bvxor64(p1: bv64, p2: bv64) : bv64;
+
+function {:bvbuiltin "bvuge"} $bv_bvuge64(p1: bv64, p2: bv64) : bool;
+
+function {:bvbuiltin "bvugt"} $bv_bvugt64(p1: bv64, p2: bv64) : bool;
+
+function {:bvbuiltin "bvsub"} $bv_bvsub64(p1: bv64, p2: bv64) : bv64;
+
+function {:bvbuiltin "bvadd"} $bv_bvadd64(p1: bv64, p2: bv64) : bv64;
+