@ @ requires \valid(fr); @ requires \valid(fr->handle); @ requires \valid(ext); @ requires fr->file_size < 0x8000000000000000 + 4; @ requires \separated(fr, fr->handle, ext, &errno, &Frama_C_entropy_source, first_filename + (..), &msoffice, &sh3d, &ext_msoffice, &expected_compressed_size); @ requires *ext == \null || *ext == extension_apk || *ext == extension_bbdoc || *e
| 602 | @ assigns expected_compressed_size; |
| 603 | @*/ |
| 604 | static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const unsigned int file_nbr) |
| 605 | { |
| 606 | char b_file[sizeof(zip_file_entry_t)]; |
| 607 | char b_extra[sizeof(zip64_extra_entry_t)]; |
| 608 | const zip_file_entry_t *file=(const zip_file_entry_t *)&b_file; |
| 609 | const zip64_extra_entry_t *extra=(const zip64_extra_entry_t *)&b_extra; |
| 610 | /*@ assert \valid_read(file); */ |
| 611 | /*@ assert \valid_read(extra); */ |
| 612 | uint64_t len; |
| 613 | if (fread(b_file, sizeof(b_file), 1, fr->handle) != 1) |
| 614 | { |
| 615 | #ifdef DEBUG_ZIP |
| 616 | log_trace("zip: Unexpected EOF reading header of file_entry\n"); |
| 617 | #endif |
| 618 | return -1; |
| 619 | } |
| 620 | #if defined(__FRAMAC__) |
| 621 | Frama_C_make_unknown(&b_file, sizeof(zip_file_entry_t)); |
| 622 | #endif |
| 623 | fr->file_size += sizeof(zip_file_entry_t); |
| 624 | #ifdef DEBUG_ZIP |
| 625 | log_info("%u Comp=%u %u CRC32=0x%08X extra_length=%u ", |
| 626 | le32(file->compressed_size), |
| 627 | le16(file->compression), |
| 628 | le32(file->uncompressed_size), |
| 629 | le32(file->crc32), |
| 630 | le16(file->extra_length)); |
| 631 | #endif |
| 632 | /* Avoid Jan 1 1980 files */ |
| 633 | if(le16(file->last_mod_time)!=0 || le16(file->last_mod_date)!=33) |
| 634 | { |
| 635 | /* Use the more recent file to set the time/date of the recovered archive */ |
| 636 | const time_t tmp=date_dos2unix(le16(file->last_mod_time), le16(file->last_mod_date)); |
| 637 | if(fr->time < tmp) |
| 638 | fr->time=tmp; |
| 639 | } |
| 640 | if(fr->file_size + 65535 >= 0x8000000000000000) |
| 641 | { |
| 642 | return -1; |
| 643 | } |
| 644 | /*@ assert fr->file_size < 0x8000000000000000 - 65535; */ |
| 645 | len = le16(file->filename_length); |
| 646 | if (len) |
| 647 | { |
| 648 | /*@ assert 0 < len <= 65535; */ |
| 649 | if(zip_parse_file_entry_fn(fr, ext, file_nbr, file, len) < 0) |
| 650 | return -1; |
| 651 | /*@ assert fr->file_size < 0x8000000000000000; */ |
| 652 | } |
| 653 | /*@ assert fr->file_size < 0x8000000000000000; */ |
| 654 | #ifdef DEBUG_ZIP |
| 655 | log_info("\n"); |
| 656 | #endif |
| 657 | len = le16(file->extra_length); |
| 658 | memset(&b_extra, 0, sizeof(zip64_extra_entry_t)); |
| 659 | if (len>0) |
| 660 | { |
| 661 | /*@ assert 0 < len <= 65535; */ |
no test coverage detected