@ @ requires \valid(fr); @ requires \valid(fr->handle); @ requires fr->file_size < 0x8000000000000000; @ requires \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ ensures \result == -1 || \result == 0; @ assigns Frama_C_entropy_source, errno; @ assigns *fr->handle, fr->file_size; @*/
| 764 | @ assigns *fr->handle, fr->file_size; |
| 765 | @*/ |
| 766 | static int zip_parse_central_dir(file_recovery_t *fr) |
| 767 | { |
| 768 | char buf_file[sizeof(zip_file_entry_t)]; |
| 769 | char buf_dir[sizeof(struct zip_central_dir)]; |
| 770 | const struct zip_central_dir *dir=(const struct zip_central_dir *)&buf_dir; |
| 771 | /*@ assert \valid_read(dir); */ |
| 772 | const zip_file_entry_t *file=(const zip_file_entry_t *)&buf_file; |
| 773 | /*@ assert \valid_read(file); */ |
| 774 | uint32_t len; |
| 775 | if (my_fseek(fr->handle, 2, SEEK_CUR) == -1) |
| 776 | { |
| 777 | #ifdef DEBUG_ZIP |
| 778 | log_trace("Unexpected EOF skipping version from central_dir\n"); |
| 779 | #endif |
| 780 | return -1; |
| 781 | } |
| 782 | fr->file_size += 2; |
| 783 | |
| 784 | if (fread(&buf_file, sizeof(zip_file_entry_t), 1, fr->handle) != 1) |
| 785 | { |
| 786 | #ifdef DEBUG_ZIP |
| 787 | log_trace("Unexpected EOF reading 1st part of central_dir\n"); |
| 788 | #endif |
| 789 | return -1; |
| 790 | } |
| 791 | #if defined(__FRAMAC__) |
| 792 | Frama_C_make_unknown(&buf_file, sizeof(zip_file_entry_t)); |
| 793 | #endif |
| 794 | fr->file_size += sizeof(zip_file_entry_t); |
| 795 | #ifdef DEBUG_ZIP |
| 796 | log_trace("zip: Central dir with CRC 0x%08X\n", file->crc32); |
| 797 | #endif |
| 798 | |
| 799 | if (fread(&buf_dir, sizeof(struct zip_central_dir), 1, fr->handle) != 1) |
| 800 | { |
| 801 | #ifdef DEBUG_ZIP |
| 802 | log_trace("zip: Unexpected EOF reading 2nd part of central_dir\n"); |
| 803 | #endif |
| 804 | return -1; |
| 805 | } |
| 806 | #if defined(__FRAMAC__) |
| 807 | Frama_C_make_unknown(&buf_dir, sizeof(struct zip_central_dir)); |
| 808 | #endif |
| 809 | fr->file_size += sizeof(struct zip_central_dir); |
| 810 | |
| 811 | /* Rest of the block - could attempt CRC check */ |
| 812 | len = le16(file->extra_length) + le16(dir->comment_length) + le16(file->filename_length); |
| 813 | if (my_fseek(fr->handle, len, SEEK_CUR) == -1) |
| 814 | { |
| 815 | #ifdef DEBUG_ZIP |
| 816 | log_trace("zip: Unexpected EOF in central_dir: %u bytes expected\n", len); |
| 817 | #endif |
| 818 | return -1; |
| 819 | } |
| 820 | fr->file_size += len; |
| 821 | #ifdef DEBUG_ZIP |
| 822 | log_trace("zip: Data of total length %u\n", len); |
| 823 | #endif |
no test coverage detected