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/lock/Lock.bpl          | 248 ++++++++++++++++++++++----------------------
 Test/lock/LockIncorrect.bpl | 106 +++++++++----------
 2 files changed, 177 insertions(+), 177 deletions(-)

(limited to 'Test/lock')

diff --git a/Test/lock/Lock.bpl b/Test/lock/Lock.bpl
index 54cd4853..515be9f0 100644
--- a/Test/lock/Lock.bpl
+++ b/Test/lock/Lock.bpl
@@ -1,124 +1,124 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure LockingExample();
-
-implementation LockingExample()
-{
-var x: int;
-var y: int;
-var held: int;
-
-start:
-  held := 0;
-  x := 0;
-  goto LoopHead;
-
-LoopHead:
-  // Lock
-  assert held == 0;
-  held := 1;
-
-  y := x;
-  goto UnlockNow, LoopEnd;
-
-UnlockNow:
-  // Unlock
-  assert held == 1;
-  held := 0;
-
-  x := x + 1;
-  goto LoopEnd;
-
-LoopEnd:
-  goto ContinueIteration, EndIteration;
-
-ContinueIteration:
-  assume x != y;
-  goto LoopHead;
-
-EndIteration:
-  assume x == y;
-  goto AfterLoop;
-
-AfterLoop:
-  // Unlock
-  assert held == 1;
-  held := 0;
-
-  return;
-
-}
-
-
-procedure StructuredLockingExample()
-{
-  var x: int;
-  var y: int;
-  var held: bool;
-
-  held := false;
-  x := 0;
-
-  while (true)
-    invariant !held;
-  {
-    // Lock
-    assert !held;
-    held := true;
-
-    y := x;
-    if (*) {
-      // Unlock
-      assert held;
-      held := false;
-
-      x := x + 1;
-    }
-
-    if (x == y) { break; }
-  }
-
-  // Unlock
-  assert held;
-  held := false;
-}
-
-procedure StructuredLockingExampleWithCalls()
-{
-  var x: int;
-  var y: int;
-  var mutex: Mutex;
-
-  call mutex := Initialize();
-  x := 0;
-
-  while (true)
-    invariant !IsHeld(mutex);
-  {
-    call mutex := Acquire(mutex);
-
-    y := x;
-    if (*) {
-      call mutex := Release(mutex);
-      x := x + 1;
-    }
-
-    if (x == y) { break; }
-  }
-
-  call mutex := Release(mutex);
-}
-
-type Mutex;
-function IsHeld(Mutex) returns (bool);
-
-procedure Initialize() returns (post: Mutex);
-  ensures !IsHeld(post);
-
-procedure Acquire(pre: Mutex) returns (post: Mutex);
-  requires !IsHeld(pre);
-  ensures IsHeld(post);
-
-procedure Release(pre: Mutex) returns (post: Mutex);
-  requires IsHeld(pre);
-  ensures !IsHeld(post);
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure LockingExample();
+
+implementation LockingExample()
+{
+var x: int;
+var y: int;
+var held: int;
+
+start:
+  held := 0;
+  x := 0;
+  goto LoopHead;
+
+LoopHead:
+  // Lock
+  assert held == 0;
+  held := 1;
+
+  y := x;
+  goto UnlockNow, LoopEnd;
+
+UnlockNow:
+  // Unlock
+  assert held == 1;
+  held := 0;
+
+  x := x + 1;
+  goto LoopEnd;
+
+LoopEnd:
+  goto ContinueIteration, EndIteration;
+
+ContinueIteration:
+  assume x != y;
+  goto LoopHead;
+
+EndIteration:
+  assume x == y;
+  goto AfterLoop;
+
+AfterLoop:
+  // Unlock
+  assert held == 1;
+  held := 0;
+
+  return;
+
+}
+
+
+procedure StructuredLockingExample()
+{
+  var x: int;
+  var y: int;
+  var held: bool;
+
+  held := false;
+  x := 0;
+
+  while (true)
+    invariant !held;
+  {
+    // Lock
+    assert !held;
+    held := true;
+
+    y := x;
+    if (*) {
+      // Unlock
+      assert held;
+      held := false;
+
+      x := x + 1;
+    }
+
+    if (x == y) { break; }
+  }
+
+  // Unlock
+  assert held;
+  held := false;
+}
+
+procedure StructuredLockingExampleWithCalls()
+{
+  var x: int;
+  var y: int;
+  var mutex: Mutex;
+
+  call mutex := Initialize();
+  x := 0;
+
+  while (true)
+    invariant !IsHeld(mutex);
+  {
+    call mutex := Acquire(mutex);
+
+    y := x;
+    if (*) {
+      call mutex := Release(mutex);
+      x := x + 1;
+    }
+
+    if (x == y) { break; }
+  }
+
+  call mutex := Release(mutex);
+}
+
+type Mutex;
+function IsHeld(Mutex) returns (bool);
+
+procedure Initialize() returns (post: Mutex);
+  ensures !IsHeld(post);
+
+procedure Acquire(pre: Mutex) returns (post: Mutex);
+  requires !IsHeld(pre);
+  ensures IsHeld(post);
+
+procedure Release(pre: Mutex) returns (post: Mutex);
+  requires IsHeld(pre);
+  ensures !IsHeld(post);
diff --git a/Test/lock/LockIncorrect.bpl b/Test/lock/LockIncorrect.bpl
index 4bd86bbe..db5c4b1a 100644
--- a/Test/lock/LockIncorrect.bpl
+++ b/Test/lock/LockIncorrect.bpl
@@ -1,53 +1,53 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure LockingExample();
-
-implementation LockingExample()
-{
-var x: int;
-var y: int;
-var held: int;
-
-start:
-  held := 0;
-  x := 0;
-  goto LoopHead;
-
-LoopHead:
-  // Lock
-  held := held + 6;
-  assert held == 0;
-  held := 1;
-
-  y := x;
-  goto UnlockNow, LoopEnd;
-
-UnlockNow:
-  // Unlock
-  assert held == 1;
-  held := 0;
-
-  x := x + 1;
-  goto LoopEnd;
-
-LoopEnd:
-  goto ContinueIteration, EndIteration;
-
-ContinueIteration:
-  assume x != y;
-  goto LoopHead;
-
-EndIteration:
-  assume x == y;
-  goto AfterLoop;
-
-AfterLoop:
-  // Unlock
-  assert held == 1;
-  held := 0;
-
-  return;
-
-}
-
- 
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure LockingExample();
+
+implementation LockingExample()
+{
+var x: int;
+var y: int;
+var held: int;
+
+start:
+  held := 0;
+  x := 0;
+  goto LoopHead;
+
+LoopHead:
+  // Lock
+  held := held + 6;
+  assert held == 0;
+  held := 1;
+
+  y := x;
+  goto UnlockNow, LoopEnd;
+
+UnlockNow:
+  // Unlock
+  assert held == 1;
+  held := 0;
+
+  x := x + 1;
+  goto LoopEnd;
+
+LoopEnd:
+  goto ContinueIteration, EndIteration;
+
+ContinueIteration:
+  assume x != y;
+  goto LoopHead;
+
+EndIteration:
+  assume x == y;
+  goto AfterLoop;
+
+AfterLoop:
+  // Unlock
+  assert held == 1;
+  held := 0;
+
+  return;
+
+}
+
+ 
-- 
cgit v1.2.3