@ @ requires \valid(IN); @ requires \valid_read(header); @ requires le32(header->num_FAT_blocks) > 0; @ requires 0 <= le32(header->num_extra_FAT_blocks)<= 50; @ requires 9 == le16(header->uSectorShift) || 12 == le16(header->uSectorShift); @ requires le32(header->num_FAT_blocks) <= 109+le32(header->num_extra_FAT_blocks)*((1< uSectorShift))/4-1); @ requires \separated(IN,
| 132 | @ ensures \result==\null || \initialized((char *)\result + (0 .. (le32(header->num_FAT_blocks)<<le16(header->uSectorShift))-1)); |
| 133 | @*/ |
| 134 | static uint32_t *OLE_load_FAT(FILE *IN, const struct OLE_HDR *header, const uint64_t offset) |
| 135 | { |
| 136 | char *data; |
| 137 | uint32_t *fat; |
| 138 | const uint32_t *dif; |
| 139 | const unsigned int uSectorShift=le16(header->uSectorShift); |
| 140 | const unsigned int num_FAT_blocks=le32(header->num_FAT_blocks); |
| 141 | const unsigned int num_extra_FAT_blocks=le32(header->num_extra_FAT_blocks); |
| 142 | /*@ assert uSectorShift == le16(header->uSectorShift); */ |
| 143 | /*@ assert num_FAT_blocks==le32(header->num_FAT_blocks); */ |
| 144 | /*@ assert num_FAT_blocks <= 109+le32(header->num_extra_FAT_blocks)*((1<<uSectorShift)/4-1); */ |
| 145 | #ifdef DISABLED_FOR_FRAMAC |
| 146 | const unsigned int dif_size=109*4+(50<<12); |
| 147 | #else |
| 148 | const unsigned int dif_size=109*4+(num_extra_FAT_blocks<<uSectorShift); |
| 149 | #endif |
| 150 | /*@ assert 109*4 <= dif_size <= 109*4+(50<<12); */ |
| 151 | data=(char *)MALLOC(dif_size); |
| 152 | /*@ assert \valid(data+(0..dif_size-1)); */ |
| 153 | dif=(const uint32_t*)data; |
| 154 | memcpy(data,(header+1),109*4); |
| 155 | if(num_extra_FAT_blocks > 0) |
| 156 | { /* Load DIF*/ |
| 157 | unsigned long int i; |
| 158 | /*@ |
| 159 | @ loop invariant 0 <= i <= num_extra_FAT_blocks; |
| 160 | @ loop variant num_extra_FAT_blocks - i; |
| 161 | @*/ |
| 162 | for(i=0; i<num_extra_FAT_blocks; i++) |
| 163 | { |
| 164 | /*@ assert i < num_extra_FAT_blocks; */ |
| 165 | const unsigned int data_offset=(109*4) + i * ((1<<uSectorShift)-4); |
| 166 | /*@ assert data_offset + 4 <= dif_size; */ |
| 167 | const unsigned int block=(i==0 ? le32(header->FAT_next_block): le32(dif[data_offset/4])); |
| 168 | if(OLE_read_block(IN, &data[data_offset], uSectorShift, block, offset) < 0) |
| 169 | { |
| 170 | free(data); |
| 171 | return NULL; |
| 172 | } |
| 173 | } |
| 174 | } |
| 175 | #ifdef DISABLED_FOR_FRAMAC |
| 176 | /*@ assert (109+50*((1<<12)/4-1))<<12 >= num_FAT_blocks<<uSectorShift; */ |
| 177 | fat=(uint32_t*)MALLOC((109+50*((1<<12)/4-1))<<12); |
| 178 | #else |
| 179 | fat=(uint32_t*)MALLOC(num_FAT_blocks<<uSectorShift); |
| 180 | #endif |
| 181 | /*@ assert \valid((char *)fat + (0 .. (num_FAT_blocks<<uSectorShift)-1)); */ |
| 182 | { /* Load FAT */ |
| 183 | unsigned int j; |
| 184 | /*@ |
| 185 | @ loop invariant 0 <= j <= num_FAT_blocks; |
| 186 | @ loop invariant j > 0 ==> \initialized((char *)fat + (0 .. (j<<uSectorShift)-1)); |
| 187 | @ loop variant num_FAT_blocks - j; |
| 188 | @*/ |
| 189 | for(j=0; j<num_FAT_blocks; j++) |
| 190 | { |
| 191 | if(OLE_read_block(IN, (char*)fat + (j<<uSectorShift), uSectorShift, le32(dif[j]), offset)<0) |
no test coverage detected