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