From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 28 Jun 2015 01:44:30 +0100
Subject: 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.

---
 Test/civl/lock2.bpl | 126 ++++++++++++++++++++++++++--------------------------
 1 file changed, 63 insertions(+), 63 deletions(-)

(limited to 'Test/civl/lock2.bpl')

diff --git a/Test/civl/lock2.bpl b/Test/civl/lock2.bpl
index 4809a8f5..e84d0a6f 100644
--- a/Test/civl/lock2.bpl
+++ b/Test/civl/lock2.bpl
@@ -1,63 +1,63 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var {:layer 0,2} b: int;
-
-procedure {:yields} {:layer 2} main()
-{
-    yield;
-    while (*)
-    {
-        async call Customer();
-        yield;
-    }
-    yield;
-}
-
-procedure {:yields} {:layer 2} Customer()
-{
-    yield;
-    while (*) 
-    {
-        call Enter();
-    	yield;
-    	call Leave();
-        yield;
-    }
-    yield;
-}
-
-procedure {:yields} {:layer 1,2} Enter() 
-ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;
-{
-    var _old, curr: int;
-    yield;
-    while (true) { 
-        call _old := CAS(0, 1);
-	yield;
-        if (_old == 0) {
-	    break;
-	}
-	while (true) {
-	    call curr := Read();
-	    yield;
-	    if (curr == 0) {
-	        break;
-	    }
-	}
-	yield;
-    }
-    yield;
-}
-
-procedure {:yields} {:layer 0,2} Read() returns (val: int);
-ensures {:atomic} |{ A: val := b; return true; }|;
-
-procedure {:yields} {:layer 0,2} CAS(prev: int, next: int) returns (_old: int);
-ensures {:atomic} |{ 
-A: _old := b; goto B, C; 
-B: assume _old == prev; b := next; return true; 
-C: assume _old != prev; return true; 
-}|;
-
-procedure {:yields} {:layer 0,2} Leave();
-ensures {:atomic} |{ A: b := 0; return true; }|;
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,2} b: int;
+
+procedure {:yields} {:layer 2} main()
+{
+    yield;
+    while (*)
+    {
+        async call Customer();
+        yield;
+    }
+    yield;
+}
+
+procedure {:yields} {:layer 2} Customer()
+{
+    yield;
+    while (*) 
+    {
+        call Enter();
+    	yield;
+    	call Leave();
+        yield;
+    }
+    yield;
+}
+
+procedure {:yields} {:layer 1,2} Enter() 
+ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;
+{
+    var _old, curr: int;
+    yield;
+    while (true) { 
+        call _old := CAS(0, 1);
+	yield;
+        if (_old == 0) {
+	    break;
+	}
+	while (true) {
+	    call curr := Read();
+	    yield;
+	    if (curr == 0) {
+	        break;
+	    }
+	}
+	yield;
+    }
+    yield;
+}
+
+procedure {:yields} {:layer 0,2} Read() returns (val: int);
+ensures {:atomic} |{ A: val := b; return true; }|;
+
+procedure {:yields} {:layer 0,2} CAS(prev: int, next: int) returns (_old: int);
+ensures {:atomic} |{ 
+A: _old := b; goto B, C; 
+B: assume _old == prev; b := next; return true; 
+C: assume _old != prev; return true; 
+}|;
+
+procedure {:yields} {:layer 0,2} Leave();
+ensures {:atomic} |{ A: b := 0; return true; }|;
-- 
cgit v1.2.3