@ @ requires \valid(disk); @ requires valid_disk(disk); @ requires \valid_read(partition); @ requires valid_partition(partition); @ requires \valid(list_search_space); @ requires \separated(disk, partition, list_search_space); @ decreases 0; @*/
| 47 | @ decreases 0; |
| 48 | @*/ |
| 49 | static void fat12_remove_used_space(disk_t *disk,const partition_t *partition, alloc_data_t *list_search_space, const unsigned int fat_offset, const unsigned int no_of_cluster, const unsigned int start_data, const unsigned int cluster_size, const unsigned int sector_size) |
| 50 | { |
| 51 | unsigned char *buffer; |
| 52 | unsigned int cluster; |
| 53 | const uint64_t hd_offset=partition->part_offset+(uint64_t)fat_offset*sector_size; |
| 54 | uint64_t start_free=0; |
| 55 | uint64_t end_free=0; |
| 56 | unsigned long int offset_s_prev=0; |
| 57 | log_trace("fat12_remove_used_space\n"); |
| 58 | buffer=(unsigned char *)MALLOC(2*sector_size); |
| 59 | del_search_space(list_search_space, partition->part_offset, |
| 60 | partition->part_offset + (uint64_t)start_data * sector_size - 1); |
| 61 | for(cluster=2; cluster<=no_of_cluster+1; cluster++) |
| 62 | { |
| 63 | unsigned long int offset_s,offset_o; |
| 64 | unsigned int next_cluster; |
| 65 | offset_s=(cluster+cluster/2)/disk->sector_size; |
| 66 | offset_o=(cluster+cluster/2)%disk->sector_size; |
| 67 | if(offset_s!=offset_s_prev || cluster==2) |
| 68 | { |
| 69 | offset_s_prev=offset_s; |
| 70 | if((unsigned)disk->pread(disk, buffer, 2*sector_size, hd_offset + offset_s * disk->sector_size) != 2*sector_size) |
| 71 | { |
| 72 | /* Consider these FAT sectors points to free clusters */ |
| 73 | } |
| 74 | } |
| 75 | if((cluster&1)!=0) |
| 76 | next_cluster=le16((*((uint16_t*)&buffer[offset_o])))>>4; |
| 77 | else |
| 78 | next_cluster=le16(*((uint16_t*)&buffer[offset_o]))&0x0FFF; |
| 79 | if(next_cluster!=0) |
| 80 | { |
| 81 | /* Not free */ |
| 82 | if(end_free+1==partition->part_offset+(start_data+(uint64_t)(cluster-2)*cluster_size)*sector_size) |
| 83 | end_free+=cluster_size*sector_size; |
| 84 | else |
| 85 | { |
| 86 | if(start_free != end_free) |
| 87 | del_search_space(list_search_space, start_free, end_free); |
| 88 | start_free=partition->part_offset+(start_data+(uint64_t)(cluster-2)*cluster_size)*sector_size; |
| 89 | end_free=start_free+(uint64_t)cluster_size*sector_size-1; |
| 90 | } |
| 91 | } |
| 92 | } |
| 93 | free(buffer); |
| 94 | if(start_free != end_free) |
| 95 | del_search_space(list_search_space, start_free, end_free); |
| 96 | } |
| 97 | |
| 98 | /*@ |
| 99 | @ requires \valid(disk_car); |
no test coverage detected