diff options
Diffstat (limited to 'src/hdwin32.h')
| -rw-r--r-- | src/hdwin32.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/hdwin32.h b/src/hdwin32.h index f78d55de..1057f68d 100644 --- a/src/hdwin32.h +++ b/src/hdwin32.h @@ -26,6 +26,10 @@ extern "C" { #endif #if defined(__CYGWIN__) || defined(__MINGW32__) +/*@ + @ requires \valid(dev); + @ requires valid_disk(dev); + @*/ void file_win32_disk_get_model(HANDLE handle, disk_t *dev, const int verbose); #endif |