diff options
Diffstat (limited to 'src/addpart.h')
| -rw-r--r-- | src/addpart.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/addpart.h b/src/addpart.h index 70d8d31c..f08d9c91 100644 --- a/src/addpart.h +++ b/src/addpart.h @@ -24,11 +24,11 @@ #define _ADDPART_H /*@ @ requires \valid(disk); - @ requires list_part == \null || \valid_read(list_part); + @ requires valid_disk(disk); + @ requires valid_list_part(list_part); @ requires \valid(current_cmd); @ requires valid_read_string(*current_cmd); @ requires separation: \separated(disk, list_part, current_cmd); - @ ensures valid_read_string(*current_cmd); @*/ list_part_t *add_partition_cli(disk_t *disk, list_part_t *list_part, char **current_cmd); #endif |