@ @ requires \valid(disk); @ requires \valid_read((const struct info_file_struct *)disk->data); @ requires valid_disk(disk); @ ensures valid_disk(disk); @*/ ensures valid_read_string(\result);
| 1324 | @*/ |
| 1325 | // ensures valid_read_string(\result); |
| 1326 | static const char *file_description(disk_t *disk) |
| 1327 | { |
| 1328 | const struct info_file_struct *data=(const struct info_file_struct *)disk->data; |
| 1329 | char buffer_disk_size[100]; |
| 1330 | #ifdef DISABLED_FOR_FRAMAC |
| 1331 | memset(&buffer_disk_size, 0, sizeof(buffer_disk_size)); |
| 1332 | #endif |
| 1333 | size_to_unit(disk->disk_size, buffer_disk_size); |
| 1334 | if(disk->geom.heads_per_cylinder == 1 && disk->geom.sectors_per_head == 1) |
| 1335 | snprintf(disk->description_txt, sizeof(disk->description_txt), |
| 1336 | "Disk %s - %s - %llu sectors%s", |
| 1337 | disk->device, buffer_disk_size, |
| 1338 | (long long unsigned)(disk->disk_size / disk->sector_size), |
| 1339 | ((data->mode&O_RDWR)==O_RDWR?"":" (RO)")); |
| 1340 | else |
| 1341 | snprintf(disk->description_txt, sizeof(disk->description_txt), |
| 1342 | "Disk %s - %s - CHS %lu %u %u%s", |
| 1343 | disk->device, buffer_disk_size, |
| 1344 | disk->geom.cylinders, disk->geom.heads_per_cylinder, disk->geom.sectors_per_head, |
| 1345 | ((data->mode&O_RDWR)==O_RDWR?"":" (RO)")); |
| 1346 | /*@ assert valid_read_string((char *)&disk->description_txt); */ |
| 1347 | /*@ assert valid_disk(disk); */ |
| 1348 | return disk->description_txt; |
| 1349 | } |
| 1350 | |
| 1351 | /*@ |
| 1352 | @ requires \valid(disk_car); |
no test coverage detected