diff options
Diffstat (limited to 'src/msdos.h')
| -rw-r--r-- | src/msdos.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/msdos.h b/src/msdos.h index 83196d6b..78724274 100644 --- a/src/msdos.h +++ b/src/msdos.h @@ -34,6 +34,11 @@ struct info_disk_struct }; disk_t *hd_identify(const int verbose, const unsigned int disk, const int testdisk_mode); + +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @*/ const char *disk_description(disk_t *disk_car); #ifdef __cplusplus |