@ @ requires buffer_size >= 85; @ requires separation: \separated(&file_hint_zip, 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); @ ensures (\result == 1) ==> (file_recovery_new->time == 0); @ ensures (\result =
| 1299 | @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension)); |
| 1300 | @*/ |
| 1301 | static int header_check_zip(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) |
| 1302 | { |
| 1303 | const zip_file_entry_t *file=(const zip_file_entry_t *)&buffer[4]; |
| 1304 | const unsigned int len=le16(file->filename_length); |
| 1305 | #ifdef DEBUG_ZIP |
| 1306 | log_trace("header_check_zip\n"); |
| 1307 | #endif |
| 1308 | if(len==0 || len > 4096) |
| 1309 | return 0; |
| 1310 | if(le16(file->version) < 10) |
| 1311 | return 0; |
| 1312 | #if !defined(SINGLE_FORMAT_zip) |
| 1313 | if(file_recovery->file_stat!=NULL && |
| 1314 | file_recovery->file_stat->file_hint==&file_hint_doc) |
| 1315 | { |
| 1316 | if(header_ignored_adv(file_recovery, file_recovery_new)==0) |
| 1317 | return 0; |
| 1318 | } |
| 1319 | #endif |
| 1320 | /* A zip file begins by ZIP_FILE_ENTRY, this signature can also be |
| 1321 | * found for each compressed file */ |
| 1322 | if(file_recovery->file_check == &file_check_zip && |
| 1323 | file_recovery->file_stat!=NULL && |
| 1324 | // file_recovery->file_stat->file_hint==&file_hint_zip && |
| 1325 | safe_header_only==0) |
| 1326 | { |
| 1327 | /*@ assert file_recovery->file_check == file_check_zip; */ |
| 1328 | if(header_ignored_adv(file_recovery, file_recovery_new)==0) |
| 1329 | return 0; |
| 1330 | } |
| 1331 | reset_file_recovery(file_recovery_new); |
| 1332 | file_recovery_new->min_filesize=30; /* 4+sizeof(file) == 30 */ |
| 1333 | file_recovery_new->file_check=&file_check_zip; |
| 1334 | if(len==8 && memcmp(&buffer[30],"mimetype",8)==0 && le16(file->extra_length)==0) |
| 1335 | { |
| 1336 | const unsigned int compressed_size=le32(file->compressed_size); |
| 1337 | file_recovery_new->extension=zip_parse_parse_entry_mimetype((const char *)&buffer[38], compressed_size); |
| 1338 | } |
| 1339 | else if(len==19 && memcmp(&buffer[30],"[Content_Types].xml",19)==0) |
| 1340 | { |
| 1341 | if(pos_in_mem(&buffer[0], buffer_size, (const unsigned char*)"word/", 5)!=0) |
| 1342 | file_recovery_new->extension=extension_docx; |
| 1343 | else if(pos_in_mem(&buffer[0], 2000, (const unsigned char*)"xl/", 3)!=0) |
| 1344 | file_recovery_new->extension=extension_xlsx; |
| 1345 | else if(pos_in_mem(&buffer[0], buffer_size, (const unsigned char*)"ppt/", 4)!=0) |
| 1346 | file_recovery_new->extension=extension_pptx; |
| 1347 | else if(pos_in_mem(&buffer[0], buffer_size, (const unsigned char*)"visio/", 6)!=0) |
| 1348 | file_recovery_new->extension=extension_vsdx; |
| 1349 | else |
| 1350 | file_recovery_new->extension=extension_docx; |
| 1351 | file_recovery_new->file_rename=&file_rename_zip; |
| 1352 | } |
| 1353 | /* Extended Renoise song file */ |
| 1354 | else if(len==8 && memcmp(&buffer[30], "Song.xml", 8)==0) |
| 1355 | file_recovery_new->extension=extension_xrns; |
| 1356 | else if(len==4 && memcmp(&buffer[30], "Home", 4)==0) |
| 1357 | file_recovery_new->extension=extension_sh3d; |
| 1358 | /* Apple Numbers */ |
no test coverage detected