@ @ requires buffer_size >= sizeof(struct OLE_HDR); @ requires \valid_read((char *)header + (0 .. buffer_size-1)); @ requires 9 == le16(header->uSectorShift) || 12 == le16(header->uSectorShift); @ requires le32(header->num_FAT_blocks)>0; @ requires 0 <= le32(header->num_extra_FAT_blocks) <= 50; @ ensures \result == \null || valid_read_string(\result); @ assigns \nothing; @*/
| 537 | @ assigns \nothing; |
| 538 | @*/ |
| 539 | static const char *ole_get_file_extension(const struct OLE_HDR *header, const unsigned int buffer_size) |
| 540 | { |
| 541 | const unsigned char *buffer=(const unsigned char *)header; |
| 542 | unsigned int fat_entries; |
| 543 | unsigned int block; |
| 544 | unsigned int i; |
| 545 | const unsigned int uSectorShift=le16(header->uSectorShift); |
| 546 | /*@ assert 9 == uSectorShift || 12 == uSectorShift; */ |
| 547 | unsigned int fat_size; |
| 548 | if(buffer_size<512) |
| 549 | return NULL; |
| 550 | /*@ assert buffer_size >= 512; */ |
| 551 | fat_size=(le32(header->num_FAT_blocks) << uSectorShift); |
| 552 | fat_entries=fat_size/4; |
| 553 | /* FFFFFFFE = ENDOFCHAIN |
| 554 | * Use a loop count i to avoid endless loop */ |
| 555 | #ifdef DEBUG_OLE |
| 556 | log_info("ole_get_file_extension root_start_block=%u, fat_entries=%u\n", le32(header->root_start_block), fat_entries); |
| 557 | #endif |
| 558 | /*@ |
| 559 | @ loop assigns block, i; |
| 560 | @ loop variant fat_entries - i; |
| 561 | @*/ |
| 562 | for(block=le32(header->root_start_block), i=0; |
| 563 | block<fat_entries && block!=0xFFFFFFFE && i<fat_entries; |
| 564 | i++) |
| 565 | { |
| 566 | const uint64_t offset_root_dir=((uint64_t)1+block)<<uSectorShift; |
| 567 | #ifdef DEBUG_OLE |
| 568 | log_info("Root Directory block=%u (0x%x)\n", block, block); |
| 569 | #endif |
| 570 | if(offset_root_dir>buffer_size-512) |
| 571 | return NULL; |
| 572 | /*@ assert offset_root_dir + 512 <= buffer_size; */ |
| 573 | { |
| 574 | unsigned int sid; |
| 575 | const struct OLE_DIR *dir_entries=(const struct OLE_DIR *)&buffer[offset_root_dir]; |
| 576 | /*@ assert \valid_read((char *)dir_entries + (0 .. 512-1)); */ |
| 577 | /*@ assert \valid_read(dir_entries + (0 .. 512/sizeof(struct OLE_DIR)-1)); */ |
| 578 | const char *ext=NULL; |
| 579 | int is_db=0; |
| 580 | /*@ |
| 581 | @ loop invariant ext == \null || ext == extension_xls || ext == extension_psmodel || ext == extension_snt; |
| 582 | @ loop assigns ext, is_db, sid; |
| 583 | @ loop variant 512/sizeof(struct OLE_DIR) - sid; |
| 584 | @*/ |
| 585 | for(sid=0; |
| 586 | sid<512/sizeof(struct OLE_DIR); |
| 587 | sid++) |
| 588 | { |
| 589 | const struct OLE_DIR *dir_entry=&dir_entries[sid]; |
| 590 | /*@ assert \valid_read(dir_entry); */ |
| 591 | if(dir_entry->type==NO_ENTRY) |
| 592 | break; |
| 593 | #ifdef DEBUG_OLE |
| 594 | { |
| 595 | unsigned int j; |
| 596 | for(j=0;j<64 && j<le16(dir_entry->namsiz) && dir_entry->name[j]!='\0';j+=2) |
no test coverage detected