diff options
Diffstat (limited to 'src/partmac.c')
| -rw-r--r-- | src/partmac.c | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/partmac.c b/src/partmac.c index a9f1cbab..eb1cbf36 100644 --- a/src/partmac.c +++ b/src/partmac.c @@ -56,6 +56,8 @@ static int check_part_mac(disk_t *disk_car, const int verbose,partition_t *parti /*@ @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ ensures valid_list_part(\result); @*/ static list_part_t *read_part_mac(disk_t *disk_car, const int verbose, const int saveheader); @@ -275,6 +277,10 @@ list_part_t *add_partition_mac_cli(disk_t *disk_car,list_part_t *list_part, char assert(current_cmd!=NULL); new_partition->part_offset=disk_car->sector_size; new_partition->part_size=disk_car->disk_size-disk_car->sector_size; + /*@ + @ loop invariant valid_list_part(list_part); + @ loop invariant valid_read_string(*current_cmd); + @ */ while(1) { skip_comma_in_command(current_cmd); @@ -310,19 +316,23 @@ list_part_t *add_partition_mac_cli(disk_t *disk_car,list_part_t *list_part, char { int insert_error=0; list_part_t *new_list_part=insert_new_partition(list_part, new_partition, 0, &insert_error); + /*@ assert valid_list_part(new_list_part); */ if(insert_error>0) { free(new_partition); + /*@ assert valid_list_part(new_list_part); */ return new_list_part; } new_partition->status=STATUS_PRIM; if(test_structure_mac(list_part)!=0) new_partition->status=STATUS_DELETED; + /*@ assert valid_list_part(new_list_part); */ return new_list_part; } else { free(new_partition); + /*@ assert valid_list_part(list_part); */ return list_part; } } |