diff options
Diffstat (limited to 'src/log_part.h')
| -rw-r--r-- | src/log_part.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/log_part.h b/src/log_part.h index 0ceadfd1..d233acfa 100644 --- a/src/log_part.h +++ b/src/log_part.h @@ -25,7 +25,18 @@ extern "C" { #endif +/*@ + @ requires \valid_read(disk); + @ requires valid_disk(disk); + @ requires \valid_read(partition); + @*/ void log_partition(const disk_t *disk, const partition_t *partition); + +/*@ + @ requires \valid_read(disk); + @ requires valid_disk(disk); + @ requires valid_list_part(list_part); + @*/ void log_all_partitions(const disk_t *disk, const list_part_t *list_part); #ifdef __cplusplus |