diff options
Diffstat (limited to 'src/intrf.h')
| -rw-r--r-- | src/intrf.h | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/intrf.h b/src/intrf.h index 2bc4f9e6..dd9cfe30 100644 --- a/src/intrf.h +++ b/src/intrf.h @@ -58,8 +58,28 @@ struct MenuItem /* '\014' == ^L */ #define key_REDRAWKEY '\014' +/*@ + @ requires \valid_read(disk_car); + @ requires valid_disk(disk_car); + @*/ void log_CHS_from_LBA(const disk_t *disk_car, const unsigned long int pos_LBA); + +/*@ + @ requires \valid_read(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid_read(partition); + @ requires valid_partition(partition); + @ requires \separated(disk_car, partition); + @*/ const char *aff_part_aux(const unsigned int newline, const disk_t *disk_car, const partition_t *partition); + +/*@ + @ requires \valid_read(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid_read(partition); + @ requires valid_partition(partition); + @ requires \separated(disk_car, partition); + @*/ void aff_part_buffer(const unsigned int newline, const disk_t *disk_car, const partition_t *partition); /*@ @@ -77,6 +97,12 @@ uint64_t ask_number_cli(char **current_cmd, const uint64_t val_cur, const uint64 void screen_buffer_reset(void); int screen_buffer_add(const char *_format, ...) __attribute__ ((format (printf, 1, 2))); void screen_buffer_to_log(void); + +/*@ + @ requires \valid_read(partition); + @ requires valid_partition(partition); + @ assigns \nothing; + @*/ int get_partition_status(const partition_t *partition); #ifdef __cplusplus |