summaryrefslogtreecommitdiffstats
path: root/src/ntfsp.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/ntfsp.h')
-rw-r--r--src/ntfsp.h11
1 files changed, 10 insertions, 1 deletions
diff --git a/src/ntfsp.h b/src/ntfsp.h
index c63698f0..fde1e1fb 100644
--- a/src/ntfsp.h
+++ b/src/ntfsp.h
@@ -25,7 +25,16 @@
extern "C" {
#endif
-unsigned int ntfs_remove_used_space(disk_t *disk_car,const partition_t *partition, alloc_data_t *list_search_space);
+#if defined(HAVE_LIBNTFS) || defined(HAVE_LIBNTFS3G)
+/*@
+ @ requires \valid(disk_car);
+ @ requires valid_disk(disk_car);
+ @ requires valid_list_search_space(list_search_space);
+ @ requires \separated(disk_car, partition, list_search_space);
+ @ ensures valid_list_search_space(list_search_space);
+ @*/
+unsigned int ntfs_remove_used_space(disk_t *disk_car, const partition_t *partition, alloc_data_t *list_search_space);
+#endif
#ifdef __cplusplus
} /* closing brace for extern "C" */