diff options
Diffstat (limited to 'src/partsun.c')
| -rw-r--r-- | src/partsun.c | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/partsun.c b/src/partsun.c index 93e14002..b8fbb4d3 100644 --- a/src/partsun.c +++ b/src/partsun.c @@ -62,7 +62,9 @@ static int get_geometry_from_sunmbr(const unsigned char *buffer, const int verbo /*@ @ requires \valid(disk_car); + @ requires valid_disk(disk_car); @*/ +// ensures valid_list_part(\result); static list_part_t *read_part_sun(disk_t *disk_car, const int verbose, const int saveheader); /*@ @@ -87,7 +89,6 @@ static void set_next_status_sun(const disk_t *disk_car, partition_t *partition); /*@ @ requires list_part == \null || \valid_read(list_part); - @ assigns \nothing; @*/ static int test_structure_sun(const list_part_t *list_part); @@ -200,6 +201,7 @@ static list_part_t *read_part_sun(disk_t *disk_car, const int verbose, const int sun_disklabel *sunlabel; list_part_t *new_list_part=NULL; unsigned char *buffer; + /*@ assert valid_list_part(new_list_part); */ if(disk_car->sector_size < DEFAULT_SECTOR_SIZE) return NULL; buffer=(unsigned char *)MALLOC(disk_car->sector_size); @@ -217,6 +219,9 @@ static list_part_t *read_part_sun(disk_t *disk_car, const int verbose, const int free(buffer); return NULL; } + /*@ + @ loop invariant valid_list_part(new_list_part); + @*/ for(i=0;i<8;i++) { if (sunlabel->partitions[i].num_sectors > 0 @@ -238,6 +243,7 @@ static list_part_t *read_part_sun(disk_t *disk_car, const int verbose, const int } } free(buffer); + /*@ assert valid_list_part(new_list_part); */ return new_list_part; } @@ -294,7 +300,10 @@ list_part_t *add_partition_sun_cli(const disk_t *disk_car,list_part_t *list_part end.cylinder=disk_car->geom.cylinders-1; end.head=disk_car->geom.heads_per_cylinder-1; end.sector=disk_car->geom.sectors_per_head; - /*@ loop invariant valid_read_string(*current_cmd); */ + /*@ + @ loop invariant valid_list_part(list_part); + @ loop invariant valid_read_string(*current_cmd); + @ */ while(1) { skip_comma_in_command(current_cmd); @@ -315,19 +324,23 @@ list_part_t *add_partition_sun_cli(const disk_t *disk_car,list_part_t *list_part { 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_sun(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; } } |