@ @ requires buffer_size >= sizeof(struct fat_boot_sector); @ requires separation: \separated(&file_hint_fat, buffer+(..), file_recovery, file_recovery_new); @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); @ ensures valid_header_check_result(\result, file_recovery_new); @ assigns *file_recovery_new; @*/
| 75 | @ assigns *file_recovery_new; |
| 76 | @*/ |
| 77 | static int header_check_fat(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new) |
| 78 | { |
| 79 | const struct fat_boot_sector *fat_header=(const struct fat_boot_sector *)buffer; |
| 80 | uint64_t start_fat1,start_data,part_size; |
| 81 | unsigned long int no_of_cluster,fat_length,fat_length_calc; |
| 82 | const unsigned int sector_size=fat_sector_size(fat_header); |
| 83 | if(!(le16(fat_header->marker)==0xAA55 |
| 84 | && (fat_header->ignored[0]==0xeb || fat_header->ignored[0]==0xe9) |
| 85 | && (fat_header->fats==1 || fat_header->fats==2))) |
| 86 | return 0; /* Obviously not a FAT */ |
| 87 | if(!((fat_header->ignored[0]==0xeb && fat_header->ignored[2]==0x90)||fat_header->ignored[0]==0xe9)) |
| 88 | return 0; |
| 89 | if(sector_size==0 || sector_size%512!=0) |
| 90 | return 0; |
| 91 | /*@ assert sector_size >= 512; */ |
| 92 | switch(fat_header->sectors_per_cluster) |
| 93 | { |
| 94 | case 1: |
| 95 | case 2: |
| 96 | case 4: |
| 97 | case 8: |
| 98 | case 16: |
| 99 | case 32: |
| 100 | case 64: |
| 101 | case 128: |
| 102 | break; |
| 103 | default: |
| 104 | return 0; |
| 105 | } |
| 106 | /*@ assert fat_header->sectors_per_cluster != 0; */ |
| 107 | if(fat_header->fats!=1 && fat_header->fats!=2) |
| 108 | return 0; |
| 109 | /*@ assert fat_header->fats==1 || fat_header->fats==2; */ |
| 110 | if(fat_header->media!=0xF0 && fat_header->media<0xF8) |
| 111 | return 0; |
| 112 | fat_length=le16(fat_header->fat_length)>0?le16(fat_header->fat_length):le32(fat_header->fat32_length); |
| 113 | part_size=(fat_sectors(fat_header)>0?fat_sectors(fat_header):le32(fat_header->total_sect)); |
| 114 | start_fat1=le16(fat_header->reserved); |
| 115 | start_data=start_fat1+fat_header->fats*fat_length+(get_dir_entries(fat_header)*32+sector_size-1)/sector_size; |
| 116 | if(part_size < start_data) |
| 117 | return 0; |
| 118 | /*@ assert part_size >= start_data; */ |
| 119 | no_of_cluster=(part_size-start_data)/fat_header->sectors_per_cluster; |
| 120 | if(no_of_cluster<4085) |
| 121 | { |
| 122 | /* FAT12 */ |
| 123 | if((get_dir_entries(fat_header)==0)||(get_dir_entries(fat_header)%16!=0)) |
| 124 | return 0; |
| 125 | if((le16(fat_header->fat_length)>256)||(le16(fat_header->fat_length)==0)) |
| 126 | return 0; |
| 127 | fat_length_calc=((no_of_cluster+2+sector_size*2/3-1)*3/2/sector_size); |
| 128 | } |
| 129 | else if(no_of_cluster<65525) |
| 130 | { |
| 131 | /* FAT16 */ |
| 132 | if(le16(fat_header->fat_length)==0) |
| 133 | return 0; |
| 134 | if((get_dir_entries(fat_header)==0)||(get_dir_entries(fat_header)%16!=0)) |
nothing calls this directly
no test coverage detected