@ @ requires \valid(disk); @ requires valid_disk(disk); @ requires \valid_read(partition); @ requires valid_partition(partition); @ requires \separated(disk, partition); @ decreases 0; @*/
| 320 | @ decreases 0; |
| 321 | @*/ |
| 322 | static unsigned int get_next_cluster_fat12(disk_t *disk, const partition_t *partition, const int offset, const unsigned int cluster) |
| 323 | { |
| 324 | unsigned int next_cluster; |
| 325 | unsigned long int offset_s; |
| 326 | unsigned long int offset_o; |
| 327 | unsigned char *buffer=(unsigned char*)MALLOC(2*disk->sector_size); |
| 328 | offset_s=(cluster+cluster/2)/disk->sector_size; |
| 329 | offset_o=(cluster+cluster/2)%disk->sector_size; |
| 330 | if((unsigned)disk->pread(disk, buffer, 2 * disk->sector_size, |
| 331 | partition->part_offset + (uint64_t)(offset + offset_s) * disk->sector_size) != 2 * disk->sector_size) |
| 332 | { |
| 333 | #ifndef DISABLED_FOR_FRAMAC |
| 334 | log_error("get_next_cluster_fat12 read error\n"); |
| 335 | #endif |
| 336 | free(buffer); |
| 337 | return 0; |
| 338 | } |
| 339 | if((cluster&1)!=0) |
| 340 | next_cluster=le16((*((uint16_t*)&buffer[offset_o])))>>4; |
| 341 | else |
| 342 | next_cluster=le16(*((uint16_t*)&buffer[offset_o]))&0x0FFF; |
| 343 | free(buffer); |
| 344 | return next_cluster; |
| 345 | } |
| 346 | |
| 347 | /*@ |
| 348 | @ requires \valid(disk); |
no test coverage detected