diff options
| author |  qadeer <unknown> | 2014-01-02 21:30:43 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-01-02 21:30:43 -0800 |
| commit | 4a8e72a6446b09b63e28a8c16af47e67913d1801 (patch) | |
| tree | 3250eee4aeb94ecef12210b05687391664fa1122 /Test/og/DeviceCache.bpl | |
| parent | 3eaed4317fed313e56d85b7775a229f2a6c1cd01 (diff) | |
some more fixes to examples
Diffstat (limited to 'Test/og/DeviceCache.bpl')
| -rw-r--r-- | Test/og/DeviceCache.bpl | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index 7e299db0..15a99343 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -155,7 +155,6 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize); j := j + 1;
par tid := YieldToReadCache(tid);
}
- par tid := YieldToReadCache(tid);
}
procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);
|