diff options
Diffstat (limited to 'src/hdcache.h')
| -rw-r--r-- | src/hdcache.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/hdcache.h b/src/hdcache.h index c2d9b238..d263f4bc 100644 --- a/src/hdcache.h +++ b/src/hdcache.h @@ -27,6 +27,7 @@ extern "C" { /*@ @ requires \valid(disk_car); + @ requires valid_disk(disk_car); @ ensures \valid(\result); @*/ disk_t *new_diskcache(disk_t *disk_car, const unsigned int cache_size_min); |