diff options
author | qadeer <unknown> | 2013-12-29 19:36:20 -0800 |
---|---|---|
committer | qadeer <unknown> | 2013-12-29 19:36:20 -0800 |
commit | 73ead90c119797eae9042cc30ff338baf819a92f (patch) | |
tree | a2f8fb4f15ccb5abbb71cafd299409a4ac490e61 | |
parent | 17ba37afd6b86b8854c7d18f45ea8ad3ea9a150b (diff) |
made some fixes
-rw-r--r-- | Test/og/lock.bpl | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl index c00560fe..69aba91e 100644 --- a/Test/og/lock.bpl +++ b/Test/og/lock.bpl @@ -20,20 +20,22 @@ procedure {:yields} {:stable} Customer() call Leave();
}
+
+ yield;
}
procedure {:yields} Enter()
ensures {:atomic 1} |{ A: assume !b; b := true; return true; }|;
{
var status: bool;
+ yield;
L:
- yield;
call status := CAS(false, true);
+ yield;
goto A, B;
A:
assume status;
- yield;
return;
B:
|