summaryrefslogtreecommitdiff
path: root/Test/lock/LockIncorrect.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/lock/LockIncorrect.bpl')
-rw-r--r--Test/lock/LockIncorrect.bpl106
1 files changed, 53 insertions, 53 deletions
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;
+
+}
+
+