summaryrefslogtreecommitdiffstats
path: root/src/partmacn.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/partmacn.h')
-rw-r--r--src/partmacn.h5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/partmacn.h b/src/partmacn.h
index 802629cc..39b5fb8c 100644
--- a/src/partmacn.h
+++ b/src/partmacn.h
@@ -27,6 +27,11 @@ extern "C" {
#endif
void write_part_mac_warning_ncurses(void);
+/*@
+ @ requires valid_disk(disk);
+ @ requires valid_list_part(list_part);
+ @ ensures valid_list_part(list_part);
+ @*/
list_part_t *add_partition_mac_ncurses(disk_t *disk, list_part_t *list_part);
#ifdef __cplusplus