diff options
Diffstat (limited to 'src/diskacc.h')
| -rw-r--r-- | src/diskacc.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/diskacc.h b/src/diskacc.h index 28a1f348..cdaff79e 100644 --- a/src/diskacc.h +++ b/src/diskacc.h @@ -25,6 +25,11 @@ extern "C" { #endif +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \separated(disk_car, current_cmd); + @*/ int interface_check_disk_access(disk_t *disk_car, char **current_cmd); #ifdef __cplusplus |