diff options
Diffstat (limited to 'src/exfatp.h')
| -rw-r--r-- | src/exfatp.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/exfatp.h b/src/exfatp.h index 05d0d215..f31d323a 100644 --- a/src/exfatp.h +++ b/src/exfatp.h @@ -25,6 +25,15 @@ extern "C" { #endif +/*@ + @ requires \valid(disk); + @ requires valid_disk(disk); + @ requires \valid_read(partition); + @ requires valid_partition(partition); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(disk, partition, list_search_space); + @*/ +// ensures valid_list_search_space(list_search_space); unsigned int exfat_remove_used_space(disk_t *disk, const partition_t *partition, alloc_data_t *list_search_space); #ifdef __cplusplus |