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

diff --git a/Test/civl/lock-introduced.bpl b/Test/civl/lock-introduced.bpl
index c9650215..fa0a3977 100644
--- a/Test/civl/lock-introduced.bpl
+++ b/Test/civl/lock-introduced.bpl
@@ -1,100 +1,100 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

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

-function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-type X;

-const nil: X;

-var {:layer 0,2} b: bool;

-var {:layer 1,3} lock: X;

-

-procedure {:yields} {:layer 3} Customer({:linear "tid"} tid: X)

-requires {:layer 2} tid != nil; 

-requires {:layer 2} InvLock(lock, b);

-ensures {:layer 2} InvLock(lock, b);

-{

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-    while (*) 

-    invariant {:layer 2} InvLock(lock, b);

-    {

-        call Enter(tid);

-    	call Leave(tid);

-        yield;

-	assert {:layer 2} InvLock(lock, b);

-    }    

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-}

-

-function {:inline} InvLock(lock: X, b: bool) : bool

-{

-    lock != nil <==> b

-}

-

-procedure {:yields} {:layer 2,3} Enter({:linear "tid"} tid: X)

-requires {:layer 2} tid != nil; 

-requires {:layer 2} InvLock(lock, b);

-ensures {:layer 2} InvLock(lock, b);

-ensures {:right} |{ A: assume lock == nil && tid != nil; lock := tid; return true; }|;

-{

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-    call LowerEnter(tid);

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-}

-

-procedure {:yields} {:layer 2,3} Leave({:linear "tid"} tid:X)

-requires {:layer 2} InvLock(lock, b);

-ensures {:layer 2} InvLock(lock, b);

-ensures {:atomic} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;

-{

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-    call LowerLeave();

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-}

-

-procedure {:yields} {:layer 1,2} LowerEnter({:linear "tid"} tid: X) 

-ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;

-{

-    var status: bool;

-    yield;

-    L: 

-        call status := CAS(false, true);

-	yield;

-        goto A, B;

-

-    A: 

-        assume status;

-	yield;

-	return;

-

-    B:

-        assume !status;

-	goto L;

-}

-

-procedure {:yields} {:layer 1,2} LowerLeave()

-ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;

-{

-    yield;

-    call SET(false);

-    yield;

-}

-

-procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool);

-ensures {:atomic} |{ 

-A: goto B, C; 

-B: assume b == prev; b := next; status := true; return true; 

-C: status := false; return true; 

-}|;

-

-procedure {:yields} {:layer 0,1} SET(next: bool);

-ensures {:atomic} |{ A: b := next; return true; }|;

-

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+type X;
+const nil: X;
+var {:layer 0,2} b: bool;
+var {:layer 1,3} lock: X;
+
+procedure {:yields} {:layer 3} Customer({:linear "tid"} tid: X)
+requires {:layer 2} tid != nil; 
+requires {:layer 2} InvLock(lock, b);
+ensures {:layer 2} InvLock(lock, b);
+{
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+    while (*) 
+    invariant {:layer 2} InvLock(lock, b);
+    {
+        call Enter(tid);
+    	call Leave(tid);
+        yield;
+	assert {:layer 2} InvLock(lock, b);
+    }    
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+}
+
+function {:inline} InvLock(lock: X, b: bool) : bool
+{
+    lock != nil <==> b
+}
+
+procedure {:yields} {:layer 2,3} Enter({:linear "tid"} tid: X)
+requires {:layer 2} tid != nil; 
+requires {:layer 2} InvLock(lock, b);
+ensures {:layer 2} InvLock(lock, b);
+ensures {:right} |{ A: assume lock == nil && tid != nil; lock := tid; return true; }|;
+{
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+    call LowerEnter(tid);
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+}
+
+procedure {:yields} {:layer 2,3} Leave({:linear "tid"} tid:X)
+requires {:layer 2} InvLock(lock, b);
+ensures {:layer 2} InvLock(lock, b);
+ensures {:atomic} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;
+{
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+    call LowerLeave();
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+}
+
+procedure {:yields} {:layer 1,2} LowerEnter({:linear "tid"} tid: X) 
+ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
+{
+    var status: bool;
+    yield;
+    L: 
+        call status := CAS(false, true);
+	yield;
+        goto A, B;
+
+    A: 
+        assume status;
+	yield;
+	return;
+
+    B:
+        assume !status;
+	goto L;
+}
+
+procedure {:yields} {:layer 1,2} LowerLeave()
+ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;
+{
+    yield;
+    call SET(false);
+    yield;
+}
+
+procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool);
+ensures {:atomic} |{ 
+A: goto B, C; 
+B: assume b == prev; b := next; status := true; return true; 
+C: status := false; return true; 
+}|;
+
+procedure {:yields} {:layer 0,1} SET(next: bool);
+ensures {:atomic} |{ A: b := next; return true; }|;
+