summaryrefslogtreecommitdiffstats
path: root/src/ntfs_fix.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/ntfs_fix.h')
-rw-r--r--src/ntfs_fix.h6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/ntfs_fix.h b/src/ntfs_fix.h
index cb69c15b..8bf18cff 100644
--- a/src/ntfs_fix.h
+++ b/src/ntfs_fix.h
@@ -25,6 +25,12 @@
extern "C" {
#endif
+/*@
+ @ requires \valid(disk_car);
+ @ requires valid_disk(disk_car);
+ @ requires \valid(partition);
+ @ requires \separated(disk_car, partition);
+ @*/
int repair_MFT(disk_t *disk_car, partition_t *partition, const int verbose, const unsigned int expert, char **current_cmd);
#ifdef __cplusplus