diff options
Diffstat (limited to 'src/hdaccess.h')
| -rw-r--r-- | src/hdaccess.h | 36 |
1 files changed, 14 insertions, 22 deletions
diff --git a/src/hdaccess.h b/src/hdaccess.h index f1431b03..81d1c011 100644 --- a/src/hdaccess.h +++ b/src/hdaccess.h @@ -26,9 +26,11 @@ extern "C" { #endif /*@ @ requires \valid(disk_car); + @ requires valid_disk(disk_car); @ requires disk_car->sector_size > 0; @ requires disk_car->geom.heads_per_cylinder > 0; @ requires \valid_function(disk_car->pread); + @ ensures valid_disk(disk_car); @*/ void hd_update_geometry(disk_t *disk_car, const int verbose); @@ -38,35 +40,30 @@ void hd_update_geometry(disk_t *disk_car, const int verbose); void hd_update_all_geometry(const list_disk_t * list_disk, const int verbose); /*@ - @ requires list_disk==\null || \valid_read(list_disk); - @ ensures \result==\null || \valid_read(\result); + @ requires valid_list_disk(list_disk); + @ ensures valid_list_disk(\result); @*/ list_disk_t *hd_parse(list_disk_t *list_disk, const int verbose, const int testdisk_mode); /*@ @ requires valid_read_string(device); - @ ensures \result==\null || \valid(\result); - @ ensures \result!=\null ==> (0 < \result->geom.cylinders < 0x2000000000000); - @ ensures \result!=\null ==> (0 < \result->geom.heads_per_cylinder <= 255); - @ ensures \result!=\null ==> (0 < \result->geom.sectors_per_head <= 63); - @ ensures \result!=\null ==> valid_read_string(\result->device); - @ ensures \result!=\null ==> \freeable(\result); - @ ensures \result!=\null ==> (\result->device == \null || \freeable(\result->device)); - @ ensures \result!=\null ==> (\result->model == \null || \freeable(\result->model)); - @ ensures \result!=\null ==> (\result->serial_no == \null || \freeable(\result->serial_no)); - @ ensures \result!=\null ==> (\result->fw_rev == \null || \freeable(\result->fw_rev)); - @ ensures \result!=\null ==> (\result->data == \null || \freeable(\result->data)); - @ ensures \result!=\null ==> (\result->rbuffer == \null || \freeable(\result->rbuffer)); - @ ensures \result!=\null ==> (\result->wbuffer == \null || \freeable(\result->wbuffer)); + @ ensures valid_disk(\result); + @ ensures \result!=\null ==> (0 < \result->geom.cylinders < 0x2000000000000); + @ ensures \result!=\null ==> (0 < \result->geom.heads_per_cylinder <= 255); + @ ensures \result!=\null ==> (0 < \result->geom.sectors_per_head <= 63); + @ ensures valid_disk(\result); @*/ disk_t *file_test_availability(const char *device, const int verbose, const int testdisk_mode); /*@ @ requires \valid(disk_car); + @ requires valid_disk(disk_car); @ requires 0 < disk_car->geom.heads_per_cylinder; @ requires 0 < disk_car->geom.sectors_per_head; @ requires 0 < disk_car->sector_size; @ ensures 0 < disk_car->geom.cylinders < 0x2000000000000; + @ ensures valid_disk(disk_car); + @ assigns disk_car->disk_real_size, disk_car->geom.cylinders, disk_car->disk_size; @*/ void update_disk_car_fields(disk_t *disk_car); @@ -97,14 +94,9 @@ void init_disk(disk_t *disk); /*@ @ requires \valid(disk); + @ requires valid_disk(disk); @ requires \freeable(disk); - @ requires disk->device == \null || \freeable(disk->device); - @ requires disk->model == \null || \freeable(disk->model); - @ requires disk->serial_no == \null || \freeable(disk->serial_no); - @ requires disk->fw_rev == \null || \freeable(disk->fw_rev); - @ requires disk->data == \null || \freeable(disk->data); - @ requires disk->rbuffer == \null || \freeable(disk->rbuffer); - @ requires disk->wbuffer == \null || \freeable(disk->wbuffer); + @ requires valid_disk(disk); @*/ void generic_clean(disk_t *disk); |