diff options
Diffstat (limited to 'Test/og/DeviceCacheSimplified.bpl')
| -rw-r--r-- | Test/og/DeviceCacheSimplified.bpl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl index 40a0ab1c..c89bd793 100644 --- a/Test/og/DeviceCacheSimplified.bpl +++ b/Test/og/DeviceCacheSimplified.bpl @@ -1,3 +1,5 @@ +type X;
+
function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
{
currsize <= newsize && (ghostLock == nil <==> currsize == newsize)
|