@ @ requires \valid(fr); @ requires \valid(fr->handle); @ requires \valid(ext); @ requires fr->file_size < 0x8000000000000000 - 65535; @ requires \valid_read(file); @ requires 0 < len <= 65535; @ requires \separated(fr, fr->handle, ext, file, &first_filename[0 .. 256], &errno, &Frama_C_entropy_source); @ requires *ext == \null || *ext == extension_apk || *ext == extension
| 395 | @ assigns msoffice, sh3d, ext_msoffice; |
| 396 | @*/ |
| 397 | static int zip_parse_file_entry_fn(file_recovery_t *fr, const char **ext, const unsigned int file_nbr, const zip_file_entry_t *file, const uint64_t len) |
| 398 | { |
| 399 | char filename[65535+1]; |
| 400 | if (fread(filename, len, 1, fr->handle) != 1) |
| 401 | { |
| 402 | #ifdef DEBUG_ZIP |
| 403 | log_trace("zip: Unexpected EOF in file_entry header: %lu bytes expected\n", len); |
| 404 | #endif |
| 405 | return -1; |
| 406 | } |
| 407 | #if defined(__FRAMAC__) |
| 408 | Frama_C_make_unknown(filename, 65535+1); |
| 409 | #endif |
| 410 | fr->file_size += len; |
| 411 | /*@ assert fr->file_size < 0x8000000000000000; */ |
| 412 | filename[len]='\0'; |
| 413 | if(first_filename[0]=='\0') |
| 414 | { |
| 415 | const unsigned int len_tmp=(len<255?len:255); |
| 416 | /*@ assert 0 <= len_tmp <= 255; */ |
| 417 | strncpy(first_filename, filename, len_tmp); |
| 418 | first_filename[len_tmp]='\0'; |
| 419 | } |
| 420 | #ifdef DEBUG_ZIP |
| 421 | log_info("%s (len=%lu)\n", filename, len); |
| 422 | #endif |
| 423 | if(*ext!=NULL) |
| 424 | return 0; |
| 425 | if(file_nbr==0) |
| 426 | { |
| 427 | msoffice=0; |
| 428 | sh3d=0; |
| 429 | ext_msoffice=NULL; |
| 430 | } |
| 431 | if(len==19 && memcmp(filename, "[Content_Types].xml", 19)==0) |
| 432 | msoffice=1; |
| 433 | else if(file_nbr==0) |
| 434 | { |
| 435 | if(len==8 && memcmp(filename, "mimetype", 8)==0) |
| 436 | { |
| 437 | char buffer[128]; |
| 438 | /*@ assert \valid_read(file); */ |
| 439 | const unsigned int compressed_size=le32(file->compressed_size); |
| 440 | const int to_read=(compressed_size < 128 ? compressed_size: 128); |
| 441 | const int extra_length=le16(file->extra_length); |
| 442 | if (my_fseek(fr->handle, extra_length, SEEK_CUR) < 0) |
| 443 | { |
| 444 | #ifdef DEBUG_ZIP |
| 445 | log_info("fseek failed\n"); |
| 446 | #endif |
| 447 | return -1; |
| 448 | } |
| 449 | if( fread(buffer, to_read, 1, fr->handle)!=1) |
| 450 | { |
| 451 | #ifdef DEBUG_ZIP |
| 452 | log_trace("zip: Unexpected EOF in file_entry data: %u bytes expected\n", |
| 453 | compressed_size); |
| 454 | #endif |
no test coverage detected