@ @ requires \valid(disk); @ requires valid_disk(disk); @ requires \valid_read(partition); @ requires valid_partition(partition); @ requires \separated(disk, partition); @ decreases 0; @*/
| 384 | @ decreases 0; |
| 385 | @*/ |
| 386 | static unsigned int get_next_cluster_fat32(disk_t *disk, const partition_t *partition, const int offset, const unsigned int cluster) |
| 387 | { |
| 388 | unsigned int next_cluster; |
| 389 | unsigned long int offset_s; |
| 390 | unsigned long int offset_o; |
| 391 | unsigned char *buffer=(unsigned char*)MALLOC(disk->sector_size); |
| 392 | const uint32_t *p32=(const uint32_t*)buffer; |
| 393 | offset_s=cluster/(disk->sector_size/4); |
| 394 | offset_o=cluster%(disk->sector_size/4); |
| 395 | if((unsigned)disk->pread(disk, buffer, disk->sector_size, |
| 396 | partition->part_offset + (uint64_t)(offset + offset_s) * disk->sector_size) != disk->sector_size) |
| 397 | { |
| 398 | #ifndef DISABLED_FOR_FRAMAC |
| 399 | log_error("get_next_cluster_fat32 read error\n"); |
| 400 | #endif |
| 401 | free(buffer); |
| 402 | return 0; |
| 403 | } |
| 404 | /* FAT32 used 28 bits, the 4 high bits are reserved |
| 405 | * 0x00000000: free cluster |
| 406 | * 0x0FFFFFF7: bad cluster |
| 407 | * 0x0FFFFFF8+: EOC End of cluster |
| 408 | * */ |
| 409 | next_cluster=le32(p32[offset_o])&0xFFFFFFF; |
| 410 | free(buffer); |
| 411 | return next_cluster; |
| 412 | } |
| 413 | |
| 414 | unsigned int get_next_cluster(disk_t *disk,const partition_t *partition, const upart_type_t upart_type,const int offset, const unsigned int cluster) |
| 415 | { |
no test coverage detected