@ @ requires buffer_size >= sizeof(struct OLE_HDR); @ requires separation: \separated(&file_hint_doc, 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); @ ensu
| 1810 | @ assigns *file_recovery_new; |
| 1811 | @*/ |
| 1812 | static int header_check_doc(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) |
| 1813 | { |
| 1814 | /*@ assert file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename); */ |
| 1815 | const struct OLE_HDR *header=(const struct OLE_HDR *)buffer; |
| 1816 | /* Check for Little Endian */ |
| 1817 | if(le16(header->uByteOrder)!=0xFFFE) |
| 1818 | return 0; |
| 1819 | if(le16(header->uDllVersion)!=3 && le16(header->uDllVersion)!=4) |
| 1820 | return 0; |
| 1821 | if(le16(header->reserved)!=0 || le32(header->reserved1)!=0) |
| 1822 | return 0; |
| 1823 | if(le16(header->uMiniSectorShift)!=6) |
| 1824 | return 0; |
| 1825 | if(le16(header->uDllVersion)==3 && le16(header->uSectorShift)!=9) |
| 1826 | return 0; |
| 1827 | /* max and qbb file have uSectorShift=12 */ |
| 1828 | if(le16(header->uDllVersion)==4 && le16(header->uSectorShift)!=12) |
| 1829 | return 0; |
| 1830 | if(le16(header->uDllVersion)==3 && le32(header->csectDir)!=0) |
| 1831 | return 0; |
| 1832 | /* max file have csectDir=1 |
| 1833 | * qbb file have csectDir=4 */ |
| 1834 | if(le16(header->uDllVersion)==4 && le32(header->csectDir)==0) |
| 1835 | return 0; |
| 1836 | /* |
| 1837 | num_FAT_blocks=109+num_extra_FAT_blocks*(512-1); |
| 1838 | maximum file size is 512+(num_FAT_blocks*128)*512, about 1.6GB |
| 1839 | */ |
| 1840 | if(le32(header->num_FAT_blocks)==0 || |
| 1841 | le32(header->num_extra_FAT_blocks)>50 || |
| 1842 | le32(header->num_FAT_blocks)>109+le32(header->num_extra_FAT_blocks)*((1<<le16(header->uSectorShift))/4-1)) |
| 1843 | return 0; |
| 1844 | /*@ assert file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename); */ |
| 1845 | /*@ assert le32(header->num_FAT_blocks) <= 109+le32(header->num_extra_FAT_blocks)*((1<<le16(header->uSectorShift))/4-1); */ |
| 1846 | reset_file_recovery(file_recovery_new); |
| 1847 | file_recovery_new->file_check=&file_check_doc; |
| 1848 | file_recovery_new->file_rename=&file_rename_doc; |
| 1849 | file_recovery_new->extension=ole_get_file_extension(header, buffer_size); |
| 1850 | if(file_recovery_new->extension!=NULL) |
| 1851 | { |
| 1852 | /*@ assert valid_read_string(file_recovery_new->extension); */ |
| 1853 | if(strcmp(file_recovery_new->extension,"sda")==0) |
| 1854 | { |
| 1855 | if(td_memmem(buffer,buffer_size,"StarImpress",11)!=NULL) |
| 1856 | file_recovery_new->extension=extension_sdd; |
| 1857 | } |
| 1858 | else if(strcmp(file_recovery_new->extension,"wps")==0) |
| 1859 | { |
| 1860 | /* Distinguish between MS Works .wps and MS Publisher .pub */ |
| 1861 | if(td_memmem(buffer,buffer_size,"Microsoft Publisher",19)!=NULL) |
| 1862 | file_recovery_new->extension=extension_pub; |
| 1863 | } |
| 1864 | /*@ assert valid_read_string(file_recovery_new->extension); */ |
| 1865 | return 1; |
| 1866 | } |
| 1867 | if(td_memmem(buffer,buffer_size,"WordDocument",12)!=NULL) |
| 1868 | { |
| 1869 | file_recovery_new->extension=extension_doc; |
no test coverage detected