diff options
Diffstat (limited to 'src/hidden.h')
| -rw-r--r-- | src/hidden.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/hidden.h b/src/hidden.h index 4d302bdc..f5bda2e0 100644 --- a/src/hidden.h +++ b/src/hidden.h @@ -25,6 +25,11 @@ extern "C" { #endif +/*@ + @ requires \valid_read(disk); + @ requires valid_disk(disk); + @ assigns \nothing; + @*/ int is_hpa_or_dco(const disk_t *disk); #ifdef __cplusplus |