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.

10 files changed, 328 insertions, 328 deletions

diff --git a/Test/linear/allocator.bpl b/Test/linear/allocator.bpl
index 147d700f..fcd79b26 100644
--- a/Test/linear/allocator.bpl
+++ b/Test/linear/allocator.bpl
@@ -1,12 +1,12 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"

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

-procedure A({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int);

-  ensures i == i';

-

-procedure B({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 

-{

-  i := i';

-  call i := A(i);

-  assert false;

-}

-

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure A({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int);
+  ensures i == i';
+
+procedure B({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 
+{
+  i := i';
+  call i := A(i);
+  assert false;
+}
+
diff --git a/Test/linear/async-bug.bpl b/Test/linear/async-bug.bpl
index ad7020ad..4692f267 100644
--- a/Test/linear/async-bug.bpl
+++ b/Test/linear/async-bug.bpl
@@ -1,36 +1,36 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"

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

-const GcTid:int;

-

-procedure {:yields} {:layer 100} Initialize({:linear "tid"} tid:int)

-requires{:layer 100} tid == GcTid;

-{

-    yield;

-    assert{:layer 100} tid == GcTid;

-

-    call GarbageCollect(tid);

-

-    yield;

-    assert{:layer 100} tid == GcTid;

-

-    async call GarbageCollect(tid);

-

-    yield;

-    assert{:layer 100} tid == GcTid;

-

-    async call GarbageCollect(tid);

-

-    yield;

-    assert{:layer 100} tid == GcTid;

-

-    yield;

-    assert{:layer 100} tid == GcTid;

-}

-

-procedure {:yields} {:layer 100} GarbageCollect({:linear "tid"} tid:int)

-requires{:layer 100} tid == GcTid;

-{

-    yield;

-    assert{:layer 100} tid == GcTid;

-}

-

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+const GcTid:int;
+
+procedure {:yields} {:layer 100} Initialize({:linear "tid"} tid:int)
+requires{:layer 100} tid == GcTid;
+{
+    yield;
+    assert{:layer 100} tid == GcTid;
+
+    call GarbageCollect(tid);
+
+    yield;
+    assert{:layer 100} tid == GcTid;
+
+    async call GarbageCollect(tid);
+
+    yield;
+    assert{:layer 100} tid == GcTid;
+
+    async call GarbageCollect(tid);
+
+    yield;
+    assert{:layer 100} tid == GcTid;
+
+    yield;
+    assert{:layer 100} tid == GcTid;
+}
+
+procedure {:yields} {:layer 100} GarbageCollect({:linear "tid"} tid:int)
+requires{:layer 100} tid == GcTid;
+{
+    yield;
+    assert{:layer 100} tid == GcTid;
+}
+
diff --git a/Test/linear/async-bug.bpl.expect b/Test/linear/async-bug.bpl.expect
index 73a5eaee..b27eace7 100644
--- a/Test/linear/async-bug.bpl.expect
+++ b/Test/linear/async-bug.bpl.expect
@@ -1,3 +1,3 @@
-async-bug.bpl(21,30): Error: unavailable source for a linear read

-async-bug.bpl(28,0): Error: Input variable tid must be available at a return

-2 type checking errors detected in async-bug.bpl

+async-bug.bpl(21,30): Error: unavailable source for a linear read
+async-bug.bpl(28,0): Error: Input variable tid must be available at a return
+2 type checking errors detected in async-bug.bpl
diff --git a/Test/linear/bug.bpl b/Test/linear/bug.bpl
index 9177e2ca..4757b5b9 100644
--- a/Test/linear/bug.bpl
+++ b/Test/linear/bug.bpl
@@ -1,16 +1,16 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"

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

-function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

-function {:inline} {:linear ""} LinearIntDistinctness(x:int) : [int]bool { MapConstBool(false)[x := true] }

-

-var {:linear ""} g:int;

-

-procedure A()

-{

-}

-

-procedure B()

-{

-  call A();

-  assert false;

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+function {:inline} {:linear ""} LinearIntDistinctness(x:int) : [int]bool { MapConstBool(false)[x := true] }
+
+var {:linear ""} g:int;
+
+procedure A()
+{
+}
+
+procedure B()
+{
+  call A();
+  assert false;
+}
diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl
index 0d255149..cf786143 100644
--- a/Test/linear/f1.bpl
+++ b/Test/linear/f1.bpl
@@ -1,48 +1,48 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"

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

-function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

-const {:existential true} b0: bool;

-const {:existential true} b1: bool;

-const {:existential true} b2: bool;

-const {:existential true} b3: bool;

-const {:existential true} b4: bool;

-const {:existential true} b5: bool;

-const {:existential true} b6: bool;

-const {:existential true} b7: bool;

-const {:existential true} b8: bool;

-

-axiom(b0);

-axiom(b1);

-axiom(b2);

-axiom(b3);

-axiom(b4);

-axiom(b5);

-axiom(!b6);

-axiom(!b7);

-axiom(b8);

-

-procedure main({:linear_in "1"} x_in: [int]bool) 

-  requires b0 ==> x_in == mapconstbool(true);

-  requires b1 ==> x_in != mapconstbool(false);

-{

-   var {:linear "1"} x: [int] bool;

-   x := x_in;

-

-   call foo(x);

-   

-   assert b6 ==> x == mapconstbool(true);

-   assert b7 ==> x != mapconstbool(false);

-   assert b8 ==> x == mapconstbool(false);

-}

-

-procedure foo({:linear_in "1"} x_in: [int]bool)

-  requires b2 ==> x_in == mapconstbool(true);

-  requires b3 ==> x_in != mapconstbool(false);

-{

-   var {:linear "1"} x: [int] bool;

-   x := x_in;

-

-   assert b4 ==> x == mapconstbool(true);

-   assert b5 ==> x != mapconstbool(false);

-

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true} b2: bool;
+const {:existential true} b3: bool;
+const {:existential true} b4: bool;
+const {:existential true} b5: bool;
+const {:existential true} b6: bool;
+const {:existential true} b7: bool;
+const {:existential true} b8: bool;
+
+axiom(b0);
+axiom(b1);
+axiom(b2);
+axiom(b3);
+axiom(b4);
+axiom(b5);
+axiom(!b6);
+axiom(!b7);
+axiom(b8);
+
+procedure main({:linear_in "1"} x_in: [int]bool) 
+  requires b0 ==> x_in == mapconstbool(true);
+  requires b1 ==> x_in != mapconstbool(false);
+{
+   var {:linear "1"} x: [int] bool;
+   x := x_in;
+
+   call foo(x);
+   
+   assert b6 ==> x == mapconstbool(true);
+   assert b7 ==> x != mapconstbool(false);
+   assert b8 ==> x == mapconstbool(false);
+}
+
+procedure foo({:linear_in "1"} x_in: [int]bool)
+  requires b2 ==> x_in == mapconstbool(true);
+  requires b3 ==> x_in != mapconstbool(false);
+{
+   var {:linear "1"} x: [int] bool;
+   x := x_in;
+
+   assert b4 ==> x == mapconstbool(true);
+   assert b5 ==> x != mapconstbool(false);
+
+}
diff --git a/Test/linear/f2.bpl b/Test/linear/f2.bpl
index 18f518da..f6c67873 100644
--- a/Test/linear/f2.bpl
+++ b/Test/linear/f2.bpl
@@ -1,22 +1,22 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"

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

-function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

-function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;

-

-procedure Split({:linear_in "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);

-ensures xls == mapunion(xls1, xls2) && xls1 != mapconstbool(false) && xls2 != mapconstbool(false);

-

-procedure Allocate() returns ({:linear "1"} x: [int]bool);

-

-procedure main() 

-{

-   var {:linear "1"} x: [int] bool;

-   var {:linear "1"} x1: [int] bool;

-   var {:linear "1"} x2: [int] bool;

-

-   call x := Allocate();

-   assume x == mapconstbool(true);

-

-   call x1, x2 := Split(x);

-   assert false;

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
+function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;
+
+procedure Split({:linear_in "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);
+ensures xls == mapunion(xls1, xls2) && xls1 != mapconstbool(false) && xls2 != mapconstbool(false);
+
+procedure Allocate() returns ({:linear "1"} x: [int]bool);
+
+procedure main() 
+{
+   var {:linear "1"} x: [int] bool;
+   var {:linear "1"} x1: [int] bool;
+   var {:linear "1"} x2: [int] bool;
+
+   call x := Allocate();
+   assume x == mapconstbool(true);
+
+   call x1, x2 := Split(x);
+   assert false;
+}
diff --git a/Test/linear/f3.bpl b/Test/linear/f3.bpl
index 3a0e855c..954b4a7a 100644
--- a/Test/linear/f3.bpl
+++ b/Test/linear/f3.bpl
@@ -1,10 +1,10 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"

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

-procedure A() {}

-

-procedure B({:linear_in ""} tid:int) returns({:linear ""} tid':int)

-{

-  tid' := tid;

-  call A();

-}

-

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure A() {}
+
+procedure B({:linear_in ""} tid:int) returns({:linear ""} tid':int)
+{
+  tid' := tid;
+  call A();
+}
+
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl
index 804cb7e2..e4fa23f6 100644
--- a/Test/linear/list.bpl
+++ b/Test/linear/list.bpl
@@ -1,50 +1,50 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"

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

-type X;

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;

-

-function {:inline} {:linear "Mem"} MemCollector(xs: [X]bool) : [X]bool

-{

-  xs

-}

-

-var head: X;

-var tail: X;

-var {:linear "Mem"} D: [X]bool;

-var Next:[X]X;

-const nil: X;

-

-procedure malloc() returns (x: X, {:linear "Mem"} M: [X]bool);

-ensures M == MapConstBool(false)[x := true];

-

-procedure Join({:linear_in "Mem"} A: [X]bool);

-modifies D;

-ensures MapOr(old(D), A) == D;

-

-procedure one()

-requires D[head] && D[tail];

-requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);

-ensures D[head] && D[tail];

-ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);

-ensures head != tail;

-{

-    var x: X;

-    var {:linear "Mem"} M: [X]bool;

-

-    call x, M := malloc();

-    call Join(M);

-    Next[tail] := x;

-    tail := x;

-    Next[tail] := nil;

-}

-

-procedure two()

-requires head != tail;

-requires D[head] && D[tail];

-requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);

-ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);

-ensures D[head] && D[tail];

-{

-    head := Next[head];

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
+
+function {:inline} {:linear "Mem"} MemCollector(xs: [X]bool) : [X]bool
+{
+  xs
+}
+
+var head: X;
+var tail: X;
+var {:linear "Mem"} D: [X]bool;
+var Next:[X]X;
+const nil: X;
+
+procedure malloc() returns (x: X, {:linear "Mem"} M: [X]bool);
+ensures M == MapConstBool(false)[x := true];
+
+procedure Join({:linear_in "Mem"} A: [X]bool);
+modifies D;
+ensures MapOr(old(D), A) == D;
+
+procedure one()
+requires D[head] && D[tail];
+requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures D[head] && D[tail];
+ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures head != tail;
+{
+    var x: X;
+    var {:linear "Mem"} M: [X]bool;
+
+    call x, M := malloc();
+    call Join(M);
+    Next[tail] := x;
+    tail := x;
+    Next[tail] := nil;
+}
+
+procedure two()
+requires head != tail;
+requires D[head] && D[tail];
+requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures D[head] && D[tail];
+{
+    head := Next[head];
+}
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index 5c936dd0..b4f784d3 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -1,115 +1,115 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory  "%s" > "%t"

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

-type X;

-

-procedure A()

-{

-    var {:linear "A"} a: X;

-    var {:linear "A"} b: int;

-}

-

-procedure B()

-{

-    var {:linear "B"} a: X;

-    var {:linear "B"} b: [X]bool;

-}

-

-procedure C()

-{

-    var {:linear "C"} a: X;

-    var {:linear "C"} c: [X]int;

-}

-

-function f(X): X;

-

-procedure {:yields} {:layer 1} D()

-{

-    var {:linear "D"} a: X;

-    var {:linear "D"} x: X;

-    var {:linear "D"} b: [X]bool;

-    var c: X;

-    var {:linear "D2"} d: X;

-

-    b[a] := true;

-

-    a := f(a);

-

-    a := c;

-

-    c := a;

-

-    a := d;

-

-    a := a;

-

-    a, x := x, a;

-

-    a, x := x, x;

-

-    call a, x := E(a, x);

-

-    call a, x := E(a, a);

-

-    call a, x := E(a, f(a));

-

-    call a, x := E(a, d);

-

-    call d, x := E(a, x);

-

-    call a, x := E(c, x);

-

-    call c, x := E(a, x);

-

-    yield;

-    par a := F(a) | x := F(a);

-    yield;

-}

-

-procedure {:yields} {:layer 1} E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)

-{

-    yield;

-    c := a;

-    yield;

-}

-

-procedure {:yields} {:layer 0} F({:linear_in "D"} a: X) returns ({:linear "D"} c: X);

-

-var {:linear "x"} g:int;

-

-procedure G(i:int) returns({:linear "x"} r:int)

-{

-  r := g;

-}

-

-procedure H(i:int) returns({:linear "x"} r:int)

-modifies g;

-{

-  g := r;

-}

-

-procedure {:yields} {:layer 0} I({:linear_in ""} x:int) returns({:linear ""} x':int)

-{

-  x' := x;

-}

-

-procedure {:yields} {:layer 0} J()

-{

-}

-

-procedure {:yields} {:layer 1} P1({:linear_in ""} x:int) returns({:linear ""} x':int)

-{

-  yield;

-  par x' := I(x) | J();

-  yield;

-  call x' := I(x');

-  yield;

-}

-

-procedure {:yields} {:layer 1} P2({:linear_in ""} x:int) returns({:linear ""} x':int)

-{

-  yield;

-  call x' := I(x);

-  yield;

-  par x' := I(x') | J();

-  yield;

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+
+procedure A()
+{
+    var {:linear "A"} a: X;
+    var {:linear "A"} b: int;
+}
+
+procedure B()
+{
+    var {:linear "B"} a: X;
+    var {:linear "B"} b: [X]bool;
+}
+
+procedure C()
+{
+    var {:linear "C"} a: X;
+    var {:linear "C"} c: [X]int;
+}
+
+function f(X): X;
+
+procedure {:yields} {:layer 1} D()
+{
+    var {:linear "D"} a: X;
+    var {:linear "D"} x: X;
+    var {:linear "D"} b: [X]bool;
+    var c: X;
+    var {:linear "D2"} d: X;
+
+    b[a] := true;
+
+    a := f(a);
+
+    a := c;
+
+    c := a;
+
+    a := d;
+
+    a := a;
+
+    a, x := x, a;
+
+    a, x := x, x;
+
+    call a, x := E(a, x);
+
+    call a, x := E(a, a);
+
+    call a, x := E(a, f(a));
+
+    call a, x := E(a, d);
+
+    call d, x := E(a, x);
+
+    call a, x := E(c, x);
+
+    call c, x := E(a, x);
+
+    yield;
+    par a := F(a) | x := F(a);
+    yield;
+}
+
+procedure {:yields} {:layer 1} E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
+{
+    yield;
+    c := a;
+    yield;
+}
+
+procedure {:yields} {:layer 0} F({:linear_in "D"} a: X) returns ({:linear "D"} c: X);
+
+var {:linear "x"} g:int;
+
+procedure G(i:int) returns({:linear "x"} r:int)
+{
+  r := g;
+}
+
+procedure H(i:int) returns({:linear "x"} r:int)
+modifies g;
+{
+  g := r;
+}
+
+procedure {:yields} {:layer 0} I({:linear_in ""} x:int) returns({:linear ""} x':int)
+{
+  x' := x;
+}
+
+procedure {:yields} {:layer 0} J()
+{
+}
+
+procedure {:yields} {:layer 1} P1({:linear_in ""} x:int) returns({:linear ""} x':int)
+{
+  yield;
+  par x' := I(x) | J();
+  yield;
+  call x' := I(x');
+  yield;
+}
+
+procedure {:yields} {:layer 1} P2({:linear_in ""} x:int) returns({:linear ""} x':int)
+{
+  yield;
+  call x' := I(x);
+  yield;
+  par x' := I(x') | J();
+  yield;
+}
diff --git a/Test/linear/typecheck.bpl.expect b/Test/linear/typecheck.bpl.expect
index 5466fe62..04575093 100644
--- a/Test/linear/typecheck.bpl.expect
+++ b/Test/linear/typecheck.bpl.expect
@@ -1,16 +1,16 @@
-typecheck.bpl(33,9): Error: Only simple assignment allowed on linear variable b

-typecheck.bpl(35,6): Error: Only variable can be assigned to linear variable a

-typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a

-typecheck.bpl(41,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D

-typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment

-typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter

-typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter b

-typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same

-typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same

-typecheck.bpl(59,4): Error: Only a linear argument can be passed to linear parameter a

-typecheck.bpl(64,4): Error: Linear variable a can occur only once as an input parameter of a parallel call

-typecheck.bpl(73,0): Error: Output variable d must be available at a return

-typecheck.bpl(82,0): Error: Global variable g must be available at a return

-typecheck.bpl(87,7): Error: unavailable source for a linear read

-typecheck.bpl(88,0): Error: Output variable r must be available at a return

-15 type checking errors detected in typecheck.bpl

+typecheck.bpl(33,9): Error: Only simple assignment allowed on linear variable b
+typecheck.bpl(35,6): Error: Only variable can be assigned to linear variable a
+typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a
+typecheck.bpl(41,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D
+typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment
+typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter
+typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter b
+typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same
+typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same
+typecheck.bpl(59,4): Error: Only a linear argument can be passed to linear parameter a
+typecheck.bpl(64,4): Error: Linear variable a can occur only once as an input parameter of a parallel call
+typecheck.bpl(73,0): Error: Output variable d must be available at a return
+typecheck.bpl(82,0): Error: Global variable g must be available at a return
+typecheck.bpl(87,7): Error: unavailable source for a linear read
+typecheck.bpl(88,0): Error: Output variable r must be available at a return
+15 type checking errors detected in typecheck.bpl