diff options
| author |  qadeer <unknown> | 2014-07-15 02:26:38 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-07-15 02:26:38 -0700 |
| commit | 7395870356fb83f1b7cab70c95523d1c9f5738d4 (patch) | |
| tree | b8677cada625458aacba867081549e4a784c453d /Test/og/DeviceCache.bpl | |
| parent | 85a60be8a0a7ef1438908364b7997dddc4524ed1 (diff) | |
simplified yield type chcking and added treiber stack (not fully done)
Diffstat (limited to 'Test/og/DeviceCache.bpl')
| -rw-r--r-- | Test/og/DeviceCache.bpl | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index 62101cba..e7e3abe9 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -67,6 +67,7 @@ requires {:phase 1} xls' == mapconstbool(true); yield;
assert {:phase 1} Inv(ghostLock, currsize, newsize);
}
+ yield;
}
procedure {:yields} {:phase 1} Thread({:cnst "tid"} tid: X)
|