diff options
Diffstat (limited to 'src/ntfs_dir.h')
| -rw-r--r-- | src/ntfs_dir.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/ntfs_dir.h b/src/ntfs_dir.h index a4a4757c..8f7b534e 100644 --- a/src/ntfs_dir.h +++ b/src/ntfs_dir.h @@ -25,7 +25,17 @@ extern "C" { #endif +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid_read(partition); + @ requires \separated(disk_car, partition); + @*/ dir_partition_t dir_partition_ntfs_init(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const int verbose, const int expert); + +/*@ + @ assigns \nothing; + @*/ const char*td_ntfs_version(void); #ifdef __cplusplus |