diff options
author | qadeer <unknown> | 2014-01-02 21:14:14 -0800 |
---|---|---|
committer | qadeer <unknown> | 2014-01-02 21:14:14 -0800 |
commit | 98b4265f81494493a7501e81aea19ab4aa0e156c (patch) | |
tree | 57757c940aa009af097551e339d7073ed413c038 /Test | |
parent | 74904efdc5a29d3ca4292474ffa5a6783eed7f2d (diff) |
some more fixes
Diffstat (limited to 'Test')
-rw-r--r-- | Test/og/DeviceCache.bpl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index 6bff421c..1c2efdbb 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -118,6 +118,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsiz var j: int;
tid := tid';
+ par tid := YieldToWriteCache(tid);
call tid, j := ReadCurrsize(tid);
while (j < index)
invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid';
@@ -141,6 +142,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize); var j: int;
tid := tid';
+ par tid := YieldToReadCache(tid);
j := 0;
while(j < bytesRead)
invariant {:phase 1} 0 <= j;
|