summaryrefslogtreecommitdiffstats
path: root/src/file_doc.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_doc.c')
-rw-r--r--src/file_doc.c2027
1 files changed, 1388 insertions, 639 deletions
diff --git a/src/file_doc.c b/src/file_doc.c
index 4451796..b1cd178 100644
--- a/src/file_doc.c
+++ b/src/file_doc.c
@@ -39,13 +39,11 @@
#include "memmem.h"
#include "setdate.h"
#include "file_doc.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
static void register_header_check_doc(file_stat_t *file_stat);
-static void file_check_doc(file_recovery_t *file_recovery);
-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);
-static void file_rename_doc(file_recovery_t *file_recovery);
-static uint32_t *OLE_load_FAT(FILE *IN, const struct OLE_HDR *header, const uint64_t offset);
-static uint32_t *OLE_load_MiniFAT(FILE *IN, const struct OLE_HDR *header, const uint32_t *fat, const unsigned int fat_entries, const uint64_t offset);
const file_hint_t file_hint_doc= {
.extension="doc",
@@ -56,6 +54,45 @@ const file_hint_t file_hint_doc= {
.register_header_check=&register_header_check_doc
};
+static const char *extension_albm="albm";
+static const char *extension_amb="amb";
+static const char *extension_apr="apr";
+static const char *extension_camrec="camrec";
+static const char *extension_db="db";
+static const char *extension_dgn="dgn";
+static const char *extension_emb="emb";
+static const char *extension_et="et";
+static const char *extension_fla="fla";
+static const char *extension_ipt="ipt";
+static const char *extension_jnb="jnb";
+static const char *extension_max="max";
+static const char *extension_mdb="mdb";
+static const char *extension_mws="mws";
+static const char *extension_msg="msg";
+static const char *extension_p65="p65";
+static const char *extension_ppt="ppt";
+static const char *extension_psmodel="psmodel";
+static const char *extension_pub="pub";
+static const char *extension_qbb="qbb";
+static const char *extension_qdf_backup="qdf-backup";
+static const char *extension_qpw="qpw";
+static const char *extension_rvt="rvt";
+static const char *extension_sda="sda";
+static const char *extension_sdc="sdc";
+static const char *extension_sdd="sdd";
+static const char *extension_sdw="sdw";
+#ifdef DJGPP
+static const char *extension_sldprt="sld";
+#else
+static const char *extension_sldprt="sldprt";
+#endif
+static const char *extension_snt="snt";
+static const char *extension_tcw="tcw";
+static const char *extension_vsd="vsd";
+static const char *extension_wps="wps";
+static const char *extension_xlr="xlr";
+static const char *extension_xls="xls";
+static const char *extension_wdb="wdb";
const char WilcomDesignInformationDDD[56]=
{
@@ -68,6 +105,342 @@ const char WilcomDesignInformationDDD[56]=
'D', '\0', 'D', '\0', 'D', '\0', '\0', '\0'
};
+/*@
+ @ requires \valid(IN);
+ @ requires (9 == uSectorShift) || (12 == uSectorShift);
+ @ requires \valid( buf + (0 .. (1<<uSectorShift)-1));
+ @ ensures \result == -1 || \result == 0;
+ @*/
+/* TODO: ensures \result == 0 ==> \initialized(buf + (0 .. (1<<uSectorShift)-1)); */
+static int OLE_read_block(FILE *IN, unsigned char *buf, const unsigned int uSectorShift, const unsigned int block, const uint64_t offset)
+{
+ const size_t size=1<<uSectorShift;
+ if(block==0xFFFFFFFF || block==0xFFFFFFFE)
+ return -1;
+ if(my_fseek(IN, offset + ((uint64_t)(1+block)<<uSectorShift), SEEK_SET) < 0)
+ {
+ return -1;
+ }
+ if(fread(buf, size, 1, IN)!=1)
+ {
+ return -1;
+ }
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buf, size);
+#endif
+ /* TODO: assert \initialized((char *)buf + (0 .. size-1)); */
+ return 0;
+}
+
+/*@
+ @ requires \valid_read(dir_entry);
+ @ requires \initialized(dir_entry);
+ @ ensures \result == \null || valid_read_string(\result);
+ @*/
+static const char *entry2ext(const struct OLE_DIR *dir_entry)
+{
+ switch(le16(dir_entry->namsiz))
+ {
+ case 10:
+ if(memcmp(dir_entry->name, ".\0Q\0D\0F\0\0\0",10)==0)
+ return extension_qdf_backup;
+ break;
+ case 12:
+ /* 3ds max */
+ if(memcmp(dir_entry->name, "S\0c\0e\0n\0e\0\0\0",12)==0)
+ return extension_max;
+ /* Licom AlphaCAM */
+ else if(memcmp(dir_entry->name,"L\0i\0c\0o\0m\0\0\0",12)==0)
+ return extension_amb;
+ break;
+ case 18:
+ /* Microsoft Works .wps */
+ if(memcmp(dir_entry->name,"C\0O\0N\0T\0E\0N\0T\0S\0\0\0",18)==0)
+ return extension_wps;
+ break;
+ case 20:
+ /* Page Maker */
+ if(memcmp(&dir_entry->name, "P\0a\0g\0e\0M\0a\0k\0e\0r\0\0\0", 20)==0)
+ return extension_p65;
+ break;
+ case 22:
+ /* SigmaPlot .jnb */
+ if(memcmp(dir_entry->name, "J\0N\0B\0V\0e\0r\0s\0i\0o\0n\0\0\0", 22)==0)
+ return extension_jnb;
+ /* Autodesk Inventor part ipt or iam file */
+ if(memcmp(dir_entry->name, "R\0S\0e\0S\0t\0o\0r\0a\0g\0e\0\0\0", 22)==0)
+ return extension_ipt;
+ break;
+ case 24:
+ /* HP Photosmart Photo Printing Album */
+ if(memcmp(dir_entry->name,"I\0m\0a\0g\0e\0s\0S\0t\0o\0r\0e\0\0\0",24)==0)
+ return extension_albm;
+ /* Lotus Approch */
+ if(memcmp(dir_entry->name,"A\0p\0p\0r\0o\0a\0c\0h\0D\0o\0c\0\0\0",24)==0)
+ return extension_apr;
+ break;
+ case 28:
+ /* Microsoft Works Spreadsheet or Chart */
+ if(memcmp(dir_entry->name,"W\0k\0s\0S\0S\0W\0o\0r\0k\0B\0o\0o\0k\0\0\0",28)==0)
+ return extension_xlr;
+ /* Visio */
+ else if(memcmp(dir_entry->name,"V\0i\0s\0i\0o\0D\0o\0c\0u\0m\0e\0n\0t\0\0\0",28)==0)
+ return extension_vsd;
+ /* SolidWorks */
+ else if(memcmp(&dir_entry->name,"s\0w\0X\0m\0l\0C\0o\0n\0t\0e\0n\0t\0s\0\0\0",28)==0)
+ return extension_sldprt;
+ break;
+ case 32:
+ if(memcmp(dir_entry->name, "m\0a\0n\0i\0f\0e\0s\0t\0.\0c\0a\0m\0x\0m\0l\0\0\0",32)==0)
+ return extension_camrec;
+ /* Revit */
+ if(memcmp(dir_entry->name, "R\0e\0v\0i\0t\0P\0r\0e\0v\0i\0e\0w\0004\0.\0000\0\0", 32)==0)
+ return extension_rvt;
+ break;
+ case 34:
+ if(memcmp(dir_entry->name, "S\0t\0a\0r\0C\0a\0l\0c\0D\0o\0c\0u\0m\0e\0n\0t\0\0\0",34)==0)
+ return extension_sdc;
+ break;
+ case 36:
+ if(memcmp(dir_entry->name, "f\0i\0l\0e\0_\0C\0O\0M\0P\0A\0N\0Y\0_\0F\0I\0L\0E\0\0\0", 36)==0)
+ return extension_qbb;
+ break;
+ case 38:
+ /* Quattro Pro spreadsheet */
+ if(memcmp(dir_entry->name, "N\0a\0t\0i\0v\0e\0C\0o\0n\0t\0e\0n\0t\0_\0M\0A\0I\0N\0\0\0", 38)==0)
+ return extension_qpw;
+ else if(memcmp(dir_entry->name, "S\0t\0a\0r\0W\0r\0i\0t\0e\0r\0D\0o\0c\0u\0m\0e\0n\0t\0\0\0", 38)==0)
+ return extension_sdw;
+ break;
+ case 40:
+ if(memcmp(dir_entry->name,"P\0o\0w\0e\0r\0P\0o\0i\0n\0t\0 \0D\0o\0c\0u\0m\0e\0n\0t\0\0\0", 40)==0)
+ return extension_ppt;
+ /* Outlook */
+ else if(memcmp(dir_entry->name,"_\0_\0n\0a\0m\0e\0i\0d\0_\0v\0e\0r\0s\0i\0o\0n\0001\0.\0000\0\0\0",40)==0)
+ return extension_msg;
+ break;
+ case 46:
+ if(memcmp(dir_entry->name,
+ "I\0S\0o\0l\0i\0d\0W\0o\0r\0k\0s\0I\0n\0f\0o\0r\0m\0a\0t\0i\0o\0n\0\0\0", 46)==0)
+ {
+ return extension_sldprt;
+ }
+ break;
+ case 56:
+ /* Wilcom ES Software */
+ if(memcmp(dir_entry->name, WilcomDesignInformationDDD, 56)==0)
+ return extension_emb;
+ break;
+ }
+ return NULL;
+}
+
+/*@
+ @ 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);
+ @*/
+static const char *ole_get_file_extension(const struct OLE_HDR *header, const unsigned int buffer_size)
+{
+ const unsigned char *buffer=(const unsigned char *)header;
+ unsigned int fat_entries;
+ unsigned int block;
+ unsigned int i;
+ const unsigned int uSectorShift=le16(header->uSectorShift);
+ unsigned int fat_size;
+ if(buffer_size<512)
+ return NULL;
+ /*@ assert buffer_size >= 512; */
+ fat_size=(le32(header->num_FAT_blocks) << uSectorShift);
+ fat_entries=fat_size/4;
+ /* FFFFFFFE = ENDOFCHAIN
+ * Use a loop count i to avoid endless loop */
+#ifdef DEBUG_OLE
+ log_info("ole_get_file_extension root_start_block=%u, fat_entries=%u\n", le32(header->root_start_block), fat_entries);
+#endif
+ for(block=le32(header->root_start_block), i=0;
+ block<fat_entries && block!=0xFFFFFFFE && i<fat_entries;
+ i++)
+ {
+ const uint64_t offset_root_dir=((uint64_t)1+block)<<uSectorShift;
+#ifdef DEBUG_OLE
+ log_info("Root Directory block=%u (0x%x)\n", block, block);
+#endif
+ if(offset_root_dir>buffer_size-512)
+ return NULL;
+ /*@ assert offset_root_dir + 512 <= buffer_size; */
+ {
+ unsigned int sid;
+ const struct OLE_DIR *dir_entries=(const struct OLE_DIR *)&buffer[offset_root_dir];
+ /*@ assert \valid_read((char *)dir_entries + (0 .. 512-1)); */
+ /*@ assert \valid_read(dir_entries + (0 .. 512/sizeof(struct OLE_DIR)-1)); */
+ const char *ext=NULL;
+ int is_db=0;
+ for(sid=0;
+ sid<512/sizeof(struct OLE_DIR);
+ sid++)
+ {
+ const struct OLE_DIR *dir_entry=&dir_entries[sid];
+ if(dir_entry->type==NO_ENTRY)
+ break;
+#ifdef DEBUG_OLE
+ {
+ unsigned int j;
+ for(j=0;j<64 && j<le16(dir_entry->namsiz) && dir_entry->name[j]!='\0';j+=2)
+ {
+ log_info("%c",dir_entry->name[j]);
+ }
+ for(;j<64;j+=2)
+ log_info(" ");
+ log_info(" namsiz=%u type %u", le16(dir_entry->namsiz), dir_entry->type);
+ log_info(" Flags=%s", (dir_entry->bflags==0?"Red ":"Black"));
+ log_info(" sector %u (%u bytes)\n",
+ (unsigned int)le32(dir_entry->start_block),
+ (unsigned int)le32(dir_entry->size));
+ }
+#endif
+ {
+ const char *tmp=entry2ext(dir_entry);
+ /*@ assert tmp == \null || valid_read_string(tmp); */
+ if(tmp!=NULL)
+ return tmp;
+ }
+ switch(le16(dir_entry->namsiz))
+ {
+ case 4:
+ if(sid==1 && memcmp(&dir_entry->name, "1\0\0\0", 4)==0)
+ is_db=1;
+ else if(is_db==1 && sid==2 && memcmp(&dir_entry->name, "2\0\0\0", 4)==0)
+ is_db=2;
+ break;
+ case 16:
+ if(sid==1 && memcmp(dir_entry->name, "d\0o\0c\0.\0d\0e\0t\0\0\0", 16)==0)
+ ext=extension_psmodel;
+ /* Windows Sticky Notes */
+ else if(sid==1 && memcmp(dir_entry->name, "V\0e\0r\0s\0i\0o\0n\0\0\0", 16)==0)
+ ext=extension_snt;
+ else if(is_db==1 && sid==2 && memcmp(&dir_entry->name, "C\0a\0t\0a\0l\0o\0g\0\0\0", 16)==0)
+ is_db=2;
+ break;
+ case 18:
+ /* MS Excel
+ * Note: Microsoft Works Spreadsheet contains the same signature */
+ if(memcmp(dir_entry->name, "W\0o\0r\0k\0b\0o\0o\0k\0\0\0",18)==0)
+ ext=extension_xls;
+ break;
+ case 36:
+ /* sda=StarDraw, sdd=StarImpress */
+ if(memcmp(dir_entry->name, "S\0t\0a\0r\0D\0r\0a\0w\0D\0o\0c\0u\0m\0e\0n\0t\0003\0\0\0", 36)==0)
+ return extension_sda;
+ break;
+ }
+ if(sid==1 && memcmp(&dir_entry->name, "D\0g\0n", 6)==0)
+ return extension_dgn;
+ }
+ if(ext!=NULL)
+ {
+ /*@ assert ext == extension_xls || ext == extension_psmodel || ext == extension_snt; */
+ return ext;
+ }
+ /* Thumbs.db */
+ if(is_db==2)
+ return extension_db;
+ }
+ {
+ const uint32_t *fati=(const uint32_t *)(header+1);
+ const uint64_t fat_offset=((uint64_t)1+le32(fati[0])) << uSectorShift;
+ unsigned int fat_test_size;
+ const uint32_t *val32_ptr;
+ if(fat_offset >= buffer_size)
+ return NULL;
+ /*@ assert 0 < fat_offset < buffer_size; */
+ fat_test_size=fat_offset+block*4;
+ if(fat_test_size + 4 > buffer_size)
+ return NULL;
+ /*@ assert fat_test_size + 4 <= buffer_size; */
+ val32_ptr=(const uint32_t *)&buffer[fat_test_size];
+ block=le32(*val32_ptr);
+ }
+ }
+#ifdef DEBUG_OLE
+ log_info("Root Directory end\n");
+#endif
+ return NULL;
+}
+
+/*@
+ @ requires \valid(IN);
+ @ requires \valid_read(header);
+ @ requires le32(header->num_FAT_blocks) > 0;
+ @ requires 0 <= le32(header->num_extra_FAT_blocks)<= 50;
+ @ requires 9 == le16(header->uSectorShift) || 12 == le16(header->uSectorShift);
+ @ requires le32(header->num_FAT_blocks) <= 109+le32(header->num_extra_FAT_blocks)*((1<<le16(header->uSectorShift))/4-1);
+ @ ensures \result==\null || \valid_read((const char *)\result + ( 0 .. (le32(header->num_FAT_blocks)<<le16(header->uSectorShift))-1));
+ @*/
+static uint32_t *OLE_load_FAT(FILE *IN, const struct OLE_HDR *header, const uint64_t offset)
+{
+ uint32_t *fat;
+ uint32_t *dif;
+ const unsigned int uSectorShift=le16(header->uSectorShift);
+ const unsigned int num_FAT_blocks=le32(header->num_FAT_blocks);
+ /*@ assert uSectorShift == le16(header->uSectorShift); */
+ /*@ assert num_FAT_blocks==le32(header->num_FAT_blocks); */
+ /*@ assert num_FAT_blocks <= 109+le32(header->num_extra_FAT_blocks)*((1<<uSectorShift)/4-1); */
+ const unsigned int dif_size=109*4+(le32(header->num_extra_FAT_blocks)<<uSectorShift);
+ /*@ assert 109*4 <= dif_size <= 109*4+(50<<12); */
+#ifdef __FRAMAC__
+ dif=(uint32_t*)MALLOC(109*4+(50<<12));
+#else
+ dif=(uint32_t*)MALLOC(dif_size);
+#endif
+ /*@ assert \valid((char *)dif+(0..dif_size-1)); */
+ memcpy(dif,(header+1),109*4);
+ if(le32(header->num_extra_FAT_blocks)>0)
+ { /* Load DIF*/
+ unsigned long int i;
+ for(i=0; i<le32(header->num_extra_FAT_blocks); i++)
+ {
+ const unsigned int block=(i==0 ? le32(header->FAT_next_block) : le32(dif[109+i*(((1<<uSectorShift)/4)-1)]));
+ unsigned char *data=(unsigned char*)&dif[109]+i*((1<<uSectorShift)-4);
+ if(OLE_read_block(IN, data, uSectorShift, block, offset) < 0)
+ {
+ free(dif);
+ return NULL;
+ }
+ }
+ }
+#ifdef __FRAMAC__
+ /*@ assert (109+50*((1<<12)/4-1))<<12 >= num_FAT_blocks<<uSectorShift; */
+ fat=(uint32_t*)MALLOC((109+50*((1<<12)/4-1))<<12);
+#else
+ fat=(uint32_t*)MALLOC(num_FAT_blocks<<uSectorShift);
+#endif
+ /*@ assert \valid((char *)fat + (0 .. (num_FAT_blocks<<uSectorShift)-1)); */
+ { /* Load FAT */
+ unsigned int j;
+ for(j=0; j<num_FAT_blocks; j++)
+ {
+ if(OLE_read_block(IN, (unsigned char*)fat + (j<<uSectorShift), uSectorShift, le32(dif[j]), offset)<0)
+ {
+ free(dif);
+ free(fat);
+ return NULL;
+ }
+ }
+ }
+ free(dif);
+ return fat;
+}
+
+
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ ensures \valid(file_recovery->handle);
+ @*/
void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
{
unsigned char buffer_header[512];
@@ -77,22 +450,36 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
unsigned int freesect_count=0;
const struct OLE_HDR *header=(const struct OLE_HDR*)&buffer_header;
const uint64_t doc_file_size_org=file_recovery->file_size;
+ unsigned int uSectorShift;
+ unsigned int num_FAT_blocks;
file_recovery->file_size=offset;
/*reads first sector including OLE header */
if(my_fseek(file_recovery->handle, offset, SEEK_SET) < 0 ||
fread(&buffer_header, sizeof(buffer_header), 1, file_recovery->handle) != 1)
return ;
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&buffer_header, sizeof(buffer_header));
+#endif
+ uSectorShift=le16(header->uSectorShift);
+ num_FAT_blocks=le32(header->num_FAT_blocks);
+ /* Sanity check */
+ if( uSectorShift != 9 && uSectorShift != 12)
+ return ;
+ /*@ assert 9 == uSectorShift || 12 == uSectorShift; */
#ifdef DEBUG_OLE
log_info("file_check_doc %s\n", file_recovery->filename);
- log_trace("sector size %u\n",1<<le16(header->uSectorShift));
- log_trace("num_FAT_blocks %u\n",le32(header->num_FAT_blocks));
+ log_trace("sector size %u\n",1<<uSectorShift);
+ log_trace("num_FAT_blocks %u\n",num_FAT_blocks);
log_trace("num_extra_FAT_blocks %u\n",le32(header->num_extra_FAT_blocks));
#endif
- /* Sanity check */
- if(le32(header->num_FAT_blocks)==0 ||
- le32(header->num_extra_FAT_blocks)>50 ||
- le32(header->num_FAT_blocks)>109+le32(header->num_extra_FAT_blocks)*((1<<le16(header->uSectorShift))-1))
+ if(num_FAT_blocks==0 ||
+ le32(header->num_extra_FAT_blocks)>50)
return ;
+ /*@ assert num_FAT_blocks > 0; */
+ /*@ assert 0 <= le32(header->num_extra_FAT_blocks) <= 50; */
+ if(num_FAT_blocks > 109+le32(header->num_extra_FAT_blocks)*((1<<uSectorShift)/4-1))
+ return ;
+ /*@ assert num_FAT_blocks <= 109+le32(header->num_extra_FAT_blocks)*((1<<uSectorShift)/4-1); */
if((fat=OLE_load_FAT(file_recovery->handle, header, offset))==NULL)
{
#ifdef DEBUG_OLE
@@ -101,18 +488,34 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
return ;
}
/* Search how many entries are not used at the end of the FAT */
- for(i=(le32(header->num_FAT_blocks)<<le16(header->uSectorShift))/4-1;
- i>0 && le32(fat[i])==0xFFFFFFFF;
- i--)
- freesect_count++;
- doc_file_size=offset + ((1+(le32(header->num_FAT_blocks)<<le16(header->uSectorShift))/4-freesect_count)<<le16(header->uSectorShift));
+ {
+ const unsigned int val_max=(num_FAT_blocks<<uSectorShift)/4-1;
+ /*@ assert \valid_read((char *)fat + ( 0 .. val_max)); */
+ /*@
+ @ loop invariant 0 <= freesect_count <= val_max;
+ @ loop assigns freesect_count;
+ @ loop variant val_max - freesect_count;
+ @*/
+ for(freesect_count=0; freesect_count < val_max; freesect_count++)
+ {
+ const unsigned j=val_max-freesect_count;
+ /*@ assert 0 <= j <= val_max; */
+ if(fat[j]!=0xFFFFFFFF)
+ break;
+ }
+ }
+ /*@ assert 0 <= freesect_count <= (num_FAT_blocks<<uSectorShift)/4-1; */
+ {
+ const unsigned int block=(num_FAT_blocks<<uSectorShift)/4-freesect_count;
+ doc_file_size=offset + (((uint64_t)1+block)<<uSectorShift);
+ }
if(doc_file_size > doc_file_size_org)
{
#ifdef DEBUG_OLE
log_info("doc_file_size=%llu + (1+(%u<<%u)/4-%u)<<%u\n",
(unsigned long long)offset,
- le32(header->num_FAT_blocks), le16(header->uSectorShift),
- freesect_count, le16(header->uSectorShift));
+ num_FAT_blocks, uSectorShift,
+ freesect_count, uSectorShift);
log_info("doc_file_size %llu > doc_file_size_org %llu\n",
(unsigned long long)doc_file_size, (unsigned long long)doc_file_size_org);
#endif
@@ -124,9 +527,9 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
#endif
{
unsigned int block;
- const unsigned int fat_entries=(le32(header->num_FAT_blocks)==0 ?
+ const unsigned int fat_entries=(num_FAT_blocks==0 ?
109:
- (le32(header->num_FAT_blocks)<<le16(header->uSectorShift))/4);
+ (num_FAT_blocks<<uSectorShift)/4);
#ifdef DEBUG_OLE
log_info("root_start_block=%u, fat_entries=%u\n", le32(header->root_start_block), fat_entries);
#endif
@@ -145,19 +548,15 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
free(fat);
return ;
}
- if(my_fseek(file_recovery->handle, offset + ((1+block)<<le16(header->uSectorShift)), SEEK_SET)<0)
- {
-#ifdef DEBUG_OLE
- log_info("fseek failed\n");
+#ifdef __FRAMAC__
+ dir_entries=(struct OLE_DIR *)MALLOC(1<<12);
+#else
+ dir_entries=(struct OLE_DIR *)MALLOC(1<<uSectorShift);
#endif
- free(fat);
- return ;
- }
- dir_entries=(struct OLE_DIR *)MALLOC(1<<le16(header->uSectorShift));
- if(fread(dir_entries, (1<<le16(header->uSectorShift)), 1, file_recovery->handle)!=1)
+ if(OLE_read_block(file_recovery->handle, (unsigned char *)dir_entries, uSectorShift, block, offset)<0)
{
#ifdef DEBUG_OLE
- log_info("fread failed\n");
+ log_info("OLE_read_block failed\n");
#endif
free(dir_entries);
free(fat);
@@ -165,12 +564,14 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
}
{
unsigned int sid;
- struct OLE_DIR *dir_entry;
- for(sid=0, dir_entry=dir_entries;
- sid<(1<<le16(header->uSectorShift))/sizeof(struct OLE_DIR) && dir_entry->type!=NO_ENTRY;
- sid++,dir_entry++)
+ for(sid=0;
+ sid<(1<<uSectorShift)/sizeof(struct OLE_DIR);
+ sid++)
{
- if(offset +
+ const struct OLE_DIR *dir_entry=&dir_entries[sid];
+ if(dir_entry->type==NO_ENTRY)
+ break;
+ if(offset +
le32(dir_entry->start_block) > 0 && le32(dir_entry->size) > 0 &&
((le32(dir_entry->size) >= le32(header->miniSectorCutoff)
&& le32(dir_entry->start_block) > fat_entries) ||
@@ -192,491 +593,631 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
file_recovery->file_size=doc_file_size;
}
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires file_recovery->file_check == &file_check_doc;
+ @ ensures \valid(file_recovery->handle);
+ @*/
static void file_check_doc(file_recovery_t *file_recovery)
{
file_check_doc_aux(file_recovery, 0);
}
-static const char *ole_get_file_extension(const unsigned char *buffer, const unsigned int buffer_size)
+/*@
+ @ requires \valid(IN);
+ @ requires \valid_read(fat + (0 .. fat_entries-1));
+ @ requires 9 == uSectorShift || 12 == uSectorShift;
+ @ requires 0 < len <= 1024*1024;
+ @ ensures \result!=\null ==> \valid((char *)\result + (0 .. len - 1));
+ @*/
+static void *OLE_read_stream(FILE *IN,
+ const uint32_t *fat, const unsigned int fat_entries, const unsigned int uSectorShift,
+ const unsigned int block_start, const unsigned int len, const uint64_t offset)
{
- const struct OLE_HDR *header=(const struct OLE_HDR *)buffer;
- const uint32_t *fat;
- unsigned int fat_entries;
+ //@ split uSectorShift;
+ unsigned char *dataPt;
unsigned int block;
unsigned int i;
- if(buffer_size<512)
- return NULL;
- if(le32(header->num_FAT_blocks)==0)
- {
- fat=(const uint32_t *)(header+1);
- fat_entries=109;
- }
- else
- {
- const uint32_t *fati=(const uint32_t *)(header+1);
- const unsigned int fat_offset=(1+le32(fati[0])) << le16(header->uSectorShift);
- fat=(const uint32_t *)&buffer[fat_offset];
- fat_entries=(le32(header->num_FAT_blocks) << le16(header->uSectorShift))/4;
- if(fat_offset>buffer_size)
- fat_entries=0;
- else if(fat_offset+fat_entries>buffer_size)
- fat_entries=buffer_size-fat_offset;
- }
- /* FFFFFFFE = ENDOFCHAIN
- * Use a loop count i to avoid endless loop */
-#ifdef DEBUG_OLE
- log_info("ole_get_file_extension root_start_block=%u, fat_entries=%u\n", le32(header->root_start_block), fat_entries);
+ const unsigned int i_max=((len+(1<<uSectorShift)-1) >> uSectorShift);
+#ifdef __FRAMAC__
+ dataPt=(unsigned char *)MALLOC(((1024*1024+(1<<uSectorShift)-1) >> uSectorShift) << uSectorShift);
+#else
+ dataPt=(unsigned char *)MALLOC(i_max << uSectorShift);
#endif
- for(block=le32(header->root_start_block), i=0;
- block<fat_entries && block!=0xFFFFFFFE && i<fat_entries;
- block=le32(fat[block]), i++)
+ /*@ assert \valid(dataPt + ( 0 .. len-1)); */
+ for(i=0, block=block_start;
+ i < i_max;
+ i++, block=le32(fat[block]))
{
- const unsigned int offset_root_dir=(1+block)<<le16(header->uSectorShift);
-#ifdef DEBUG_OLE
- log_info("Root Directory block=%u (0x%x)\n", block, block);
-#endif
- if(offset_root_dir>buffer_size-512)
+ if(!(block < fat_entries))
+ {
+ free(dataPt);
return NULL;
+ }
+ if(OLE_read_block(IN, &dataPt[i<<uSectorShift], uSectorShift, block, offset)<0)
{
- unsigned int sid;
- const struct OLE_DIR *dir_entry;
- const char *ext=NULL;
- int is_db=0;
- for(sid=0,dir_entry=(const struct OLE_DIR *)&buffer[offset_root_dir];
- sid<512/sizeof(struct OLE_DIR) && dir_entry->type!=NO_ENTRY;
- sid++,dir_entry++)
- {
-#ifdef DEBUG_OLE
- unsigned int j;
- for(j=0;j<64 && j<le16(dir_entry->namsiz) && dir_entry->name[j]!='\0';j+=2)
- {
- log_info("%c",dir_entry->name[j]);
- }
- for(;j<64;j+=2)
- log_info(" ");
- log_info(" namsiz=%u type %u", le16(dir_entry->namsiz), dir_entry->type);
- log_info(" Flags=%s", (dir_entry->bflags==0?"Red ":"Black"));
- log_info(" sector %u (%u bytes)\n",
- (unsigned int)le32(dir_entry->start_block),
- (unsigned int)le32(dir_entry->size));
-#endif
- if(sid==1 && memcmp(&dir_entry->name, "1\0\0\0", 4)==0)
- is_db++;
- else if(sid==2 && (memcmp(&dir_entry->name, "2\0\0\0", 4)==0 ||
- memcmp(&dir_entry->name, "C\0a\0t\0a\0l\0o\0g\0", 14)==0))
- is_db++;
- switch(le16(dir_entry->namsiz))
- {
- case 10:
- if(memcmp(dir_entry->name, ".\0Q\0D\0F\0\0\0",10)==0)
- return "qdf-backup";
- break;
- case 12:
- /* 3ds max */
- if(memcmp(dir_entry->name, "S\0c\0e\0n\0e\0\0\0",12)==0)
- return "max";
- /* Licom AlphaCAM */
- else if(memcmp(dir_entry->name,"L\0i\0c\0o\0m\0\0\0",12)==0)
- return "amb";
- break;
- case 18:
- /* MS Excel
- * Note: Microsoft Works Spreadsheet contains the same signature */
- if(memcmp(dir_entry->name, "W\0o\0r\0k\0b\0o\0o\0k\0\0\0",18)==0)
- ext="xls";
- /* Microsoft Works .wps */
- else if(memcmp(dir_entry->name,"C\0O\0N\0T\0E\0N\0T\0S\0\0\0",18)==0)
- return "wps";
- break;
- case 20:
- /* Page Maker */
- if(memcmp(&dir_entry->name, "P\0a\0g\0e\0M\0a\0k\0e\0r\0\0\0", 20)==0)
- return "p65";
- break;
- case 22:
- /* SigmaPlot .jnb */
- if(memcmp(dir_entry->name, "J\0N\0B\0V\0e\0r\0s\0i\0o\0n\0\0\0", 22)==0)
- return "jnb";
- /* Autodesk Inventor part ipt or iam file */
- if(memcmp(dir_entry->name, "R\0S\0e\0S\0t\0o\0r\0a\0g\0e\0\0\0", 22)==0)
- return "ipt";
- break;
- case 24:
- /* HP Photosmart Photo Printing Album */
- if(memcmp(dir_entry->name,"I\0m\0a\0g\0e\0s\0S\0t\0o\0r\0e\0\0\0",24)==0)
- return "albm";
- /* Lotus Approch */
- if(memcmp(dir_entry->name,"A\0p\0p\0r\0o\0a\0c\0h\0D\0o\0c\0\0\0",24)==0)
- return "apr";
- break;
- case 28:
- /* Microsoft Works Spreadsheet or Chart */
- if(memcmp(dir_entry->name,"W\0k\0s\0S\0S\0W\0o\0r\0k\0B\0o\0o\0k\0\0\0",28)==0)
- return "xlr";
- /* Visio */
- else if(memcmp(dir_entry->name,"V\0i\0s\0i\0o\0D\0o\0c\0u\0m\0e\0n\0t\0\0\0",28)==0)
- return "vsd";
- /* SolidWorks */
- else if(memcmp(&dir_entry->name,"s\0w\0X\0m\0l\0C\0o\0n\0t\0e\0n\0t\0s\0\0\0",28)==0)
- {
-#ifdef DJGPP
- return "sld";
-#else
- return "sldprt";
-#endif
- }
- break;
- case 32:
- /* Revit */
- if(memcmp(dir_entry->name, "R\0e\0v\0i\0t\0P\0r\0e\0v\0i\0e\0w\0004\0.\0000\0\0", 32)==0)
- return "rvt";
- break;
- case 34:
- if(memcmp(dir_entry->name, "S\0t\0a\0r\0C\0a\0l\0c\0D\0o\0c\0u\0m\0e\0n\0t\0\0\0",34)==0)
- return "sdc";
- break;
- case 36:
- if(memcmp(dir_entry->name, "S\0t\0a\0r\0D\0r\0a\0w\0D\0o\0c\0u\0m\0e\0n\0t\0003\0\0\0", 36)==0)
- return "sda";
- break;
- case 38:
- /* Quattro Pro spreadsheet */
- if(memcmp(dir_entry->name, "N\0a\0t\0i\0v\0e\0C\0o\0n\0t\0e\0n\0t\0_\0M\0A\0I\0N\0\0\0", 38)==0)
- return "qpw";
- else if(memcmp(dir_entry->name, "S\0t\0a\0r\0W\0r\0i\0t\0e\0r\0D\0o\0c\0u\0m\0e\0n\0t\0\0\0", 38)==0)
- return "sdw";
- break;
- case 40:
- if(memcmp(dir_entry->name,"P\0o\0w\0e\0r\0P\0o\0i\0n\0t\0 \0D\0o\0c\0u\0m\0e\0n\0t\0\0\0", 40)==0)
- return "ppt";
- /* Outlook */
- else if(memcmp(dir_entry->name,"_\0_\0n\0a\0m\0e\0i\0d\0_\0v\0e\0r\0s\0i\0o\0n\0001\0.\0000\0\0\0",40)==0)
- return "msg";
- break;
- case 46:
- if(memcmp(dir_entry->name,
- "I\0S\0o\0l\0i\0d\0W\0o\0r\0k\0s\0I\0n\0f\0o\0r\0m\0a\0t\0i\0o\0n\0\0\0", 46)==0)
- {
-#ifdef DJGPP
- return "sld";
-#else
- return "sldprt";
-#endif
- }
- break;
- case 56:
- /* Wilcom ES Software */
- if(memcmp(dir_entry->name, WilcomDesignInformationDDD, 56)==0)
- return "emb";
- break;
- }
- if(sid==1 && memcmp(&dir_entry->name, "D\0g\0n", 6)==0)
- return "dgn";
- }
- if(ext!=NULL)
- return ext;
- /* Thumbs.db */
- if(is_db==2)
- return "db";
+ free(dataPt);
+ return NULL;
}
}
-#ifdef DEBUG_OLE
- log_info("Root Directory end\n");
-#endif
- return NULL;
+ return dataPt;
}
-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)
+/*@
+ @ requires \valid(IN);
+ @ requires \valid_read(header);
+ @ requires \valid_read(fat);
+ @ requires 9 == le16(header->uSectorShift) || 12 == le16(header->uSectorShift);
+ @ requires 0 < le32(header->csectMiniFat) <= 2048;
+ @ ensures \result!=\null ==> \valid((char *)\result + (0 .. (le32(header->csectMiniFat) << le16(header->uSectorShift)) - 1));
+ @*/
+static uint32_t *OLE_load_MiniFAT(FILE *IN, const struct OLE_HDR *header, const uint32_t *fat, const unsigned int fat_entries, const uint64_t offset)
{
- const struct OLE_HDR *header=(const struct OLE_HDR *)buffer;
- /* Check for Little Endian */
- if(le16(header->uByteOrder)!=0xFFFE)
- return 0;
- if(le16(header->uDllVersion)!=3 && le16(header->uDllVersion)!=4)
- return 0;
- if(le16(header->reserved)!=0 || le32(header->reserved1)!=0)
- return 0;
- if(le16(header->uMiniSectorShift)!=6)
- return 0;
- if(le16(header->uDllVersion)==3 && le16(header->uSectorShift)!=9)
- return 0;
- /* max and qbb file have uSectorShift=12 */
- if(le16(header->uDllVersion)==4 && le16(header->uSectorShift)!=12)
- return 0;
- if(le16(header->uDllVersion)==3 && le32(header->csectDir)!=0)
- return 0;
- /* max file have csectDir=1
- * qbb file have csectDir=4 */
- if(le16(header->uDllVersion)==4 && le32(header->csectDir)==0)
- return 0;
- /*
- num_FAT_blocks=109+num_extra_FAT_blocks*(512-1);
- maximum file size is 512+(num_FAT_blocks*128)*512, about 1.6GB
- */
- if(le32(header->num_FAT_blocks)==0 ||
- le32(header->num_extra_FAT_blocks)>50 ||
- le32(header->num_FAT_blocks)>109+le32(header->num_extra_FAT_blocks)*((1<<le16(header->uSectorShift))-1))
- return 0;
- reset_file_recovery(file_recovery_new);
- file_recovery_new->file_check=&file_check_doc;
- file_recovery_new->file_rename=&file_rename_doc;
- file_recovery_new->extension=ole_get_file_extension(buffer, buffer_size);
- if(file_recovery_new->extension!=NULL)
+ uint32_t *minifat;
+ unsigned int block;
+ unsigned int i;
+ const unsigned int uSectorShift=le16(header->uSectorShift);
+ /*@ assert uSectorShift==9 || uSectorShift==12; */
+ const unsigned int csectMiniFat=le32(header->csectMiniFat);
+ if(csectMiniFat==0)
+ return NULL;
+ /*@ assert 0 < csectMiniFat; */
+ /*@ assert 0 < csectMiniFat <= 2048; */
+#ifdef __FRAMAC__
+ minifat=(uint32_t*)MALLOC(2048 << 12);
+#else
+ minifat=(uint32_t*)MALLOC(csectMiniFat << uSectorShift);
+#endif
+ block=le32(header->MiniFat_block);
+ for(i=0; i < csectMiniFat; i++)
{
- if(strcmp(file_recovery_new->extension,"sda")==0)
+ unsigned char*minifat_pos=(unsigned char*)minifat + (i << uSectorShift);
+ if(block >= fat_entries)
{
- if(td_memmem(buffer,buffer_size,"StarImpress",11)!=NULL)
- file_recovery_new->extension="sdd";
+ free(minifat);
+ return NULL;
}
- else if(strcmp(file_recovery_new->extension,"wps")==0)
+ if(OLE_read_block(IN, (unsigned char *)minifat_pos, uSectorShift, block, offset)<0)
{
- /* Distinguish between MS Works .wps and MS Publisher .pub */
- if(td_memmem(buffer,buffer_size,"Microsoft Publisher",19)!=NULL)
- file_recovery_new->extension="pub";
+ free(minifat);
+ return NULL;
}
- return 1;
+ block=le32(fat[block]);
}
- if(td_memmem(buffer,buffer_size,"WordDocument",12)!=NULL)
+ return minifat;
+}
+
+/*@
+ @ requires \valid_read((char *)buffer + (offset .. offset + 4 - 1));
+ @ requires \initialized((char *)buffer + (offset .. offset + 4 - 1));
+ @ assigns \nothing;
+ @*/
+static uint32_t get32u(const void *buffer, const unsigned int offset)
+{
+ const uint32_t *val=(const uint32_t *)((const unsigned char *)buffer+offset);
+ return le32(*val);
+}
+
+/*@
+ @ requires \valid_read((char *)buffer + (offset .. offset + 8 - 1));
+ @ requires \initialized((char *)buffer + (offset .. offset + 8 - 1));
+ @ assigns \nothing;
+ @*/
+static uint64_t get64u(const void *buffer, const unsigned int offset)
+{
+ const uint64_t *val=(const uint64_t *)((const unsigned char *)buffer+offset);
+ return le64(*val);
+}
+
+/*@
+ @ requires \valid(ext);
+ @ requires *ext == \null || valid_read_string(*ext);
+ @ requires count > 0;
+ @ requires \valid_read(software + (0 .. count-1));
+ @ ensures *ext == \null || valid_read_string(*ext);
+ @ assigns *ext;
+ @*/
+static void software2ext(const char **ext, const unsigned char *software, const unsigned int count)
+{
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ if(count>=12)
{
- file_recovery_new->extension="doc";
+ /*@ assert \valid_read(software + (0 .. count-1)); */
+ if(memcmp(software, "MicroStation", 12)==0)
+ {
+ *ext=extension_dgn;
+ /*@ assert valid_read_string(*ext); */
+ return;
+ }
}
- else if(td_memmem(buffer,buffer_size,"StarDraw",8)!=NULL)
+ if(count>=14)
{
- file_recovery_new->extension="sda";
+ /*@ assert \valid_read(software + (0 .. count-1)); */
+ if(memcmp(software, "Microsoft Word", 14)==0)
+ {
+ *ext=file_hint_doc.extension;
+ /*@ assert valid_read_string(*ext); */
+ return;
+ }
}
- else if(td_memmem(buffer,buffer_size,"StarCalc",8)!=NULL)
+ if(count>=15)
{
- file_recovery_new->extension="sdc";
+ /*@ assert \valid_read(software + (0 .. count-1)); */
+ if(memcmp(software, "Microsoft Excel", 15)==0)
+ {
+ if(*ext==NULL || strcmp(*ext,"sldprt")!=0)
+ {
+ *ext=extension_xls;
+ /*@ assert valid_read_string(*ext); */
+ }
+ return;
+ }
}
- else if(td_memmem(buffer,buffer_size,"StarImpress",11)!=NULL)
+ if(count>=20)
{
- file_recovery_new->extension="sdd";
+ /*@ assert \valid_read(software + (0 .. count-1)); */
+ if(memcmp(software, "Microsoft PowerPoint", 20)==0)
+ {
+ *ext=extension_ppt;
+ /*@ assert valid_read_string(*ext); */
+ return;
+ }
}
- else if(td_memmem(buffer,buffer_size,"Worksheet",9)!=NULL ||
- td_memmem(buffer,buffer_size,"Book",4)!=NULL ||
- td_memmem(buffer,buffer_size,"Workbook",8)!=NULL ||
- td_memmem(buffer,buffer_size,"Calc",4)!=NULL)
+ if(count>=21)
{
- file_recovery_new->extension="xls";
+ /*@ assert \valid_read(software + (0 .. count-1)); */
+ if(memcmp(software, "Microsoft Office Word", 21)==0)
+ {
+ *ext=file_hint_doc.extension;
+ /*@ assert valid_read_string(*ext); */
+ return;
+ }
}
- else if(td_memmem(buffer,buffer_size,"Power",5)!=NULL)
+ if(count==21)
{
- file_recovery_new->extension="ppt";
+ /*@ assert \valid_read(software + (0 .. count-1)); */
+ if(memcmp(software, "TurboCAD for Windows", 21)==0)
+ {
+ *ext=extension_tcw;
+ /*@ assert valid_read_string(*ext); */
+ return;
+ }
}
- else if(td_memmem(buffer,buffer_size,"AccessObjSiteData",17)!=NULL)
+ if(count==22)
{
- file_recovery_new->extension="mdb";
+ /*@ assert \valid_read(software + (0 .. count-1)); */
+ if(memcmp(software, "TurboCAD pour Windows", 22)==0)
+ {
+ *ext=extension_tcw;
+ /*@ assert valid_read_string(*ext); */
+ return;
+ }
}
- else if(td_memmem(buffer,buffer_size,"Visio",5)!=NULL)
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ return ;
+}
+
+/*@
+ @ requires count > 0;
+ @ requires \valid_read(software + (0 .. 2*count-1));
+ @ ensures \result == \null || \result == extension_et || \result == extension_psmodel;
+ @ ensures \result == \null || valid_read_string(\result);
+ @ assigns \nothing;
+ @*/
+static const char *software_uni2ext(const unsigned char *software, const unsigned int count)
+{
+ if(count>=15)
{
- file_recovery_new->extension="vsd";
+ /*@ assert \valid_read(software + (0 .. 2*count-1)); */
+ if(memcmp(software, "M\0i\0c\0r\0o\0s\0o\0f\0t\0 \0E\0x\0c\0e\0l\0", 30)==0)
+ {
+ /*@ assert valid_read_string(extension_et); */
+ return extension_et;
+ }
}
- else if(td_memmem(buffer,buffer_size,"SfxDocument",11)!=NULL)
+ if(count>=17)
{
- file_recovery_new->extension="sdw";
- }
- else if(td_memmem(buffer,buffer_size,"CPicPage",8)!=NULL)
- { /* Flash Project File */
- file_recovery_new->extension="fla";
- }
- else if(td_memmem(buffer,buffer_size,"Microsoft Publisher",19)!=NULL)
- { /* Publisher */
- file_recovery_new->extension="pub";
- }
- else if(td_memmem(buffer, buffer_size, "Microsoft Works Database", 24)!=NULL
- || td_memmem( buffer, buffer_size, "MSWorksDBDoc", 12)!=NULL)
- { /* Microsoft Works .wdb */
- file_recovery_new->extension="wdb";
- }
- else if(td_memmem(buffer,buffer_size,"MetaStock",9)!=NULL)
- { /* MetaStock */
- file_recovery_new->extension="mws";
+ /*@ assert \valid_read(software + (0 .. 2*count-1)); */
+ if(memcmp(software, "D\0e\0l\0c\0a\0m\0 \0P\0o\0w\0e\0r\0S\0H\0A\0P\0E\0", 34)==0)
+ {
+ /*@ assert valid_read_string(extension_psmodel); */
+ return extension_psmodel;
+ }
}
- else
- file_recovery_new->extension=file_hint_doc.extension;
- return 1;
+ return NULL;
}
-static uint32_t *OLE_load_FAT(FILE *IN, const struct OLE_HDR *header, const uint64_t offset)
+struct summary_entry
{
- uint32_t *fat;
- uint32_t *dif;
- dif=(uint32_t*)MALLOC(109*4+(le32(header->num_extra_FAT_blocks)<<le16(header->uSectorShift)));
- memcpy(dif,(header+1),109*4);
- if(le32(header->num_extra_FAT_blocks)>0)
- { /* Load DIF*/
- unsigned long int i;
- unsigned long int block;
- unsigned char *data=(unsigned char*)&dif[109];
- for(i=0, block=le32(header->FAT_next_block);
- i<le32(header->num_extra_FAT_blocks) && block!=0xFFFFFFFF && block!=0xFFFFFFFE;
- i++, block=le32(dif[109+i*(((1<<le16(header->uSectorShift))/4)-1)]))
+ uint32_t tag;
+ uint32_t offset;
+};
+
+/*@
+ @ requires 8 <= size <= 1024*1024;
+ @ requires \valid_read(buffer+ (0 .. size-1));
+ @ requires \initialized(buffer+ (0 .. size-1));
+ @ requires \valid(ext);
+ @ requires *ext == \null || valid_read_string(*ext);
+ @ ensures *ext == \null || valid_read_string(*ext);
+ @ assigns *ext;
+ @*/
+static void OLE_parse_software_entry(const unsigned char *buffer, const unsigned int size, const unsigned int offset, const char **ext)
+{
+ if(offset >= size - 8)
+ {
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ return ;
+ }
+ /*@ assert offset < size - 8; */
+ {
+ const unsigned int count=get32u(buffer, offset + 4);
+ const unsigned int offset_soft=offset + 8;
+ /*@ assert offset_soft == offset + 8; */
+ if(count == 0 || count > size)
{
- if(my_fseek(IN, offset + ((1+block)<<le16(header->uSectorShift)), SEEK_SET) < 0)
- {
- free(dif);
- return NULL;
- }
- if(fread(data, 1<<le16(header->uSectorShift), 1, IN)!=1)
- {
- free(dif);
- return NULL;
- }
- data+=(1<<le16(header->uSectorShift))-4;
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ return ;
}
- }
- fat=(uint32_t*)MALLOC(le32(header->num_FAT_blocks)<<le16(header->uSectorShift));
- { /* Load FAT */
- unsigned long int j;
- unsigned char *data;
- for(j=0, data=(unsigned char*)fat;
- j<le32(header->num_FAT_blocks);
- j++, data+=(1<<le16(header->uSectorShift)))
+ /*@ assert 0 < count <= size; */
+ if(offset_soft + count > size)
{
- if(my_fseek(IN, offset + ((1+le32(dif[j]))<<le16(header->uSectorShift)), SEEK_SET)<0)
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ return ;
+ }
+ /*@ assert offset_soft + count <= size; */
+ /*@ assert count <= size - offset_soft; */
+ /*@ assert \valid_read(buffer + (0 .. size-1)); */
+ /*@ assert \valid_read(buffer + (0 .. offset_soft + count -1)); */
+#ifdef DEBUG_OLE
+ {
+ unsigned int j;
+ log_info("Software ");
+ for(j=0; j<count; j++)
{
- free(dif);
- free(fat);
- return NULL;
- }
- if(fread(data, (1<<le16(header->uSectorShift)), 1, IN)!=1)
- {
- free(dif);
- free(fat);
- return NULL;
+ /*@ assert 0 <= j < count; */
+ /*@ assert offset_soft + count <= size; */
+ const unsigned int tmp=offset_soft+j;
+ /*@ assert tmp < size; */
+ log_info("%c", buffer[tmp]);
}
+ log_info("\n");
}
+#endif
+ software2ext(ext, &buffer[offset_soft], count);
+ /*@ assert *ext == \null || valid_read_string(*ext); */
}
- free(dif);
- return fat;
+ /*@ assert *ext == \null || valid_read_string(*ext); */
}
-static void *OLE_read_stream(FILE *IN,
- const uint32_t *fat, const unsigned int fat_entries, const unsigned int uSectorShift,
- const unsigned int block_start, const unsigned int len, const uint64_t offset)
+/*@
+ @ requires 8 <= size <= 1024*1024;
+ @ requires \valid_read(buffer+ (0 .. size-1));
+ @ requires \initialized(buffer+ (0 .. size-1));
+ @ requires \valid(ext);
+ @ requires *ext == \null || valid_read_string(*ext);
+ @ ensures *ext == \null || valid_read_string(*ext);
+ @ assigns *ext;
+ @*/
+static void OLE_parse_uni_software_entry(const unsigned char *buffer, const unsigned int size, const unsigned int offset, const char **ext)
{
- unsigned char *dataPt;
- unsigned int block;
- unsigned int size_read;
- dataPt=(unsigned char *)MALLOC((len+(1<<uSectorShift)-1) / (1<<uSectorShift) * (1<<uSectorShift));
- for(block=block_start, size_read=0;
- size_read < len;
- block=le32(fat[block]), size_read+=(1<<uSectorShift))
+ if(offset >= size - 8)
{
- if(!(block < fat_entries))
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ return ;
+ }
+ /*@ assert offset < size - 8; */
+ {
+ const unsigned int offset_soft=offset + 8;
+ /*@ assert offset_soft < size; */
+ const unsigned int count=get32u(buffer, offset + 4);
+ unsigned int count2;
+ if(count == 0 || count > size/2)
{
- free(dataPt);
- return NULL;
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ return ;
}
- if(my_fseek(IN, offset + ((1+block)<<uSectorShift), SEEK_SET)<0)
+ /*@ assert 0 < count <= size/2; */
+ count2=2*count;
+ /*@ assert 0 < count2 <= size; */
+ if(count2 > size - offset_soft)
{
- free(dataPt);
- return NULL;
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ return ;
}
- if(fread(&dataPt[size_read], (1<<uSectorShift), 1, IN)!=1)
+ /*@ assert count2 <= size - offset_soft; */
+ /*@ assert offset_soft + count2 <= size; */
+ /*@ assert \valid_read(buffer + (0 .. size - 1)) && \initialized(buffer + (0 .. size - 1)); */
+ /*@ assert \valid_read(buffer + (0 .. offset_soft + count2 - 1)); */
+#ifdef DEBUG_OLE
{
- free(dataPt);
- return NULL;
+ unsigned int j;
+ log_info("Software ");
+ for(j=0; j < count2; j+=2)
+ {
+ /*@ assert 0 <= j < count2; */
+ /*@ assert offset_soft + count2 <= size; */
+ const unsigned int tmp=offset_soft + j;
+ /*@ assert tmp < size; */
+ log_info("%c", buffer[tmp]);
+ }
+ log_info("\n");
}
+#endif
+ *ext=software_uni2ext(&buffer[offset_soft], count);
}
- return dataPt;
+ /*@ assert *ext == \null || valid_read_string(*ext); */
}
-static uint32_t *OLE_load_MiniFAT(FILE *IN, const struct OLE_HDR *header, const uint32_t *fat, const unsigned int fat_entries, const uint64_t offset)
+/*@
+ @ requires 8 <= size <= 1024*1024;
+ @ requires \valid_read(buffer+ (0 .. size-1));
+ @ requires \valid(title + (0 .. 1024-1));
+ @ requires valid_string(title);
+ @ requires \initialized(buffer+ (0 .. size-1));
+ @ ensures valid_string(title);
+ @ assigns *(title + (0 .. 1023));
+ @*/
+static void OLE_parse_title_entry(const unsigned char *buffer, const unsigned int size, const unsigned int offset, char *title)
{
- unsigned char*minifat_pos;
- uint32_t *minifat;
- unsigned int block;
- unsigned int i;
- if(le32(header->csectMiniFat)==0)
- return NULL;
- minifat=(uint32_t*)MALLOC(le32(header->csectMiniFat) << le16(header->uSectorShift));
- minifat_pos=(unsigned char*)minifat;
- block=le32(header->MiniFat_block);
- for(i=0; i < le32(header->csectMiniFat) && block < fat_entries; i++)
+ if(offset + 8 > size)
+ {
+ return;
+ }
+ /*@ assert offset + 8 <= size; */
{
- if(my_fseek(IN, offset + (((uint64_t)1+block) << le16(header->uSectorShift)), SEEK_SET) < 0)
+ /*@ assert \valid_read(buffer + (0 .. size - 1)); */
+ const unsigned int count=get32u(buffer, offset + 4);
+ const unsigned int offset_tmp=offset + 8;
+ const char *src=(const char *)buffer;
+ if(count <= 1 || count > size)
{
- free(minifat);
- return NULL;
+ return;
}
- if(fread(minifat_pos, 1 << le16(header->uSectorShift), 1, IN) != 1)
+ /*@ assert 1 < count <= size; */
+ /*@ assert 1 < count <= 1024*1024; */
+ if(offset_tmp + count > size)
{
- free(minifat);
- return NULL;
+ return;
}
- minifat_pos+=1 << le16(header->uSectorShift);
- block=le32(fat[block]);
+ /*@ assert offset_tmp + count <= size; */
+ /*@ assert \valid_read(src + (0 .. size - 1)); */
+ /*@ assert offset_tmp + count <= size; */
+ /*@ assert \valid_read(src + (0 .. offset_tmp + count - 1)); */
+ /*@ assert \valid_read((src + offset_tmp) + (0 .. count - 1)); */
+ /*@ assert \valid_read((src + offset_tmp) + (1 .. count - 1)); */
+ /*@ assert \valid_read((char*)src + (0 .. offset_tmp + count - 1)); */
+ /*@ assert \valid_read(((char*)(src+offset_tmp))+(0..count-1)); */
+ /*@ assert \valid_read(((char*)(src+offset_tmp))+(1..count-1)); */
+ /*@ assert \valid_read((char*)(src + offset_tmp)); */
+ /*@ assert \valid_read((char*)(src + offset_tmp)) && \valid_read(((char*)(src+offset_tmp))+(1..count-1)); */
+ /*@ assert valid_read_or_empty((void const *)(src + offset_tmp), count); */
+ /*@ assert valid_read_or_empty((void const *)(src + offset_tmp), count); */
+#ifndef __FRAMAC__
+ if(count < 1024)
+ {
+ memcpy(title, &src[offset_tmp], count);
+ title[count]='\0';
+ /*@ assert valid_string(title); */
+ }
+ else
+ {
+ memcpy(title, &src[offset_tmp], 1023);
+ title[1023]='\0';
+ /*@ assert valid_string(title); */
+ }
+#endif
+#ifdef DEBUG_OLE
+ log_info("Title %s\n", title);
+#endif
}
- return minifat;
-}
-
-static uint32_t get32u(const void *buffer, const unsigned int offset)
-{
- const uint32_t *val=(const uint32_t *)((const unsigned char *)buffer+offset);
- return le32(*val);
+ /*@ assert valid_string(title); */
}
-static uint64_t get64u(const void *buffer, const unsigned int offset)
+/*@
+ @ requires 8 <= size <= 1024*1024;
+ @ requires \valid_read(buffer+ (0 .. size-1));
+ @ requires \initialized(buffer+ (0 .. size-1));
+ @ requires \valid(file_time);
+ @ assigns *file_time;
+ @*/
+static void OLE_parse_filetime_entry(const unsigned char *buffer, const unsigned int size, const unsigned int offset, time_t *file_time)
{
- const uint64_t *val=(const uint64_t *)((const unsigned char *)buffer+offset);
- return le64(*val);
-}
-
-static void software2ext(const char **ext, const unsigned int count, const unsigned char *software)
-{
- if(count>=12 && memcmp(software, "MicroStation", 12)==0)
+ uint64_t tmp;
+ if(offset + 12 > size)
{
- *ext="dgn";
- return;
+ return ;
}
- if(count>=14 && memcmp(software, "Microsoft Word", 14)==0)
+ /*@ assert offset + 12 <= size; */
+ tmp=get64u(buffer, offset + 4);
+ tmp/=10000000;
+ if(tmp > (uint64_t)134774 * 24 * 3600)
{
- *ext="doc";
- return;
+ tmp -= (uint64_t)134774 * 24 * 3600;
+ *file_time=tmp;
}
- if(count>=15 && memcmp(software, "Microsoft Excel", 15)==0)
+}
+
+/*@
+ @ requires 8 <= size <= 1024*1024;
+ @ requires \valid_read(buffer+ (0 .. size-1));
+ @ requires \initialized(buffer+ (0 .. size-1));
+ @ requires \valid(ext);
+ @ requires \valid(title + (0 .. 1024-1));
+ @ requires \valid(file_time);
+ @ requires \valid_read(entry);
+ @ requires *ext == \null || valid_read_string(*ext);
+ @ requires valid_string(title);
+ @ requires separation: \separated(buffer+(..), ext, title + ( 0 .. 1023), file_time);
+ @ ensures *ext == \null || valid_read_string(*ext);
+ @ ensures valid_string(title);
+ @ assigns *ext, *(title + (0..1023)), *file_time;
+ @*/
+static void OLE_parse_PropertySet_entry(const unsigned char *buffer, const unsigned int size, const struct summary_entry *entry, const char **ext, char *title, time_t *file_time)
+{
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_read_string(title); */
+ const unsigned int tag=le32(entry->tag);
+ const unsigned int offset=le32(entry->offset);
+ unsigned int type;
+ if(offset >= size - 4)
{
- if(*ext==NULL || strcmp(*ext,"sldprt")!=0)
- *ext="xls";
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
return;
}
- if(count>=20 && memcmp(software, "Microsoft PowerPoint", 20)==0)
+ /*@ assert offset < size - 4; */
+ /*@ assert \valid_read(buffer + (0 .. offset + 4 - 1)); */
+ type=get32u(buffer, offset);
+#ifdef DEBUG_OLE
+ log_info("entry 0x%x, tag 0x%x, offset 0x%x, offset + 4 0x%x, type 0x%x\n",
+ entry_offset, tag, offset, offset + 4, type);
+#endif
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ /* tag: Software, type: VT_LPSTR */
+ if(tag==0x12 && type==30)
{
- *ext="ppt";
+ /*@ assert valid_string(title); */
+ OLE_parse_software_entry(buffer, size, offset, ext);
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
return;
}
- if(count>=21 && memcmp(software, "Microsoft Office Word", 21)==0)
+ /* tag: Software, type: VT_LPWSTR */
+ if(tag==0x12 && type==31)
{
- *ext="doc";
+ /*@ assert valid_string(title); */
+ OLE_parse_uni_software_entry(buffer, size, offset, ext);
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
return;
}
- if(count==21 && memcmp(software, "TurboCAD for Windows", 21)==0)
+ /* tag: title, type: VT_LPSTR */
+ if(tag==0x02 && type==30 && title[0]=='\0')
{
- *ext="tcw";
- return;
+ OLE_parse_title_entry(buffer, size, offset, title);
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ return ;
}
- if(count==22 && memcmp(software, "TurboCAD pour Windows", 22)==0)
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ /* ModifyDate, type=VT_FILETIME */
+ if(tag==0x0d && type==64)
{
- *ext="tcw";
+ OLE_parse_filetime_entry(buffer, size, offset, file_time);
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
return;
}
- return ;
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ return;
}
-static const char *software_uni2ext(const unsigned int count, const unsigned char *software)
+/*@
+ @ requires 8 <= size <= 1024*1024;
+ @ requires \valid_read(buffer+ (0 .. size-1));
+ @ requires \valid(ext);
+ @ requires \valid(title + (0 .. 1024-1));
+ @ requires \valid(file_time);
+ @ requires valid_string(title);
+ @ requires *ext == \null || valid_read_string(*ext);
+ @ requires separation: \separated(buffer+(..), ext, title + (0 .. 1023), file_time);
+ @ ensures *ext == \null || valid_read_string(*ext);
+ @ ensures valid_string(title);
+ @*/
+/*X TODO assigns *ext, *(title + (0..1023)), *file_time; */
+/*X TODO requires \initialized(buffer+ (0 .. size-1)); */
+static void OLE_parse_PropertySet(const unsigned char *buffer, const unsigned int size, const char **ext, char *title, time_t *file_time)
{
- if(count>=15 && memcmp(software, "M\0i\0c\0r\0o\0s\0o\0f\0t\0 \0E\0x\0c\0e\0l\0", 30)==0)
- return "et";
- if(count>=17 && memcmp(software, "D\0e\0l\0c\0a\0m\0 \0P\0o\0w\0e\0r\0S\0H\0A\0P\0E\0", 34)==0)
- return "psmodel";
- return NULL;
+ const struct summary_entry *entries=(const struct summary_entry *)&buffer[8];
+ const unsigned int numEntries=get32u(buffer, 4);
+ unsigned int i;
+#ifdef DEBUG_OLE
+ log_info("Property Info %u entries - %u bytes\n", numEntries, size);
+#endif
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ if(numEntries == 0 || numEntries > 1024*1024)
+ {
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ return ;
+ }
+ /*@ assert 0 < numEntries <= 1024*1024; */
+ if(8 + numEntries * 8 > size)
+ {
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ return ;
+ }
+ /*@ assert 8 + numEntries * 8 <= size; */
+ /*@ assert numEntries * 8 <= size - 8; */
+ /*@ assert numEntries < size/8; */
+ if((const unsigned char *)&entries[numEntries] > &buffer[size])
+ {
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ return ;
+ }
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ /*@ assert \valid_read(buffer + (0 .. size - 1)); */
+ /*@ assert \valid_read((buffer+8) + (8 .. size - 8 - 1)); */
+ /*@
+ @ loop invariant *ext == \null || valid_read_string(*ext);
+ @ loop invariant valid_string(title);
+ @ loop invariant 0 <= i <= numEntries;
+ @ loop variant numEntries-i;
+ @*/
+ /*X TODO loop assigns *ext, *(title + (0..1023)), *file_time; */
+ for(i=0; i<numEntries; i++)
+ {
+ const struct summary_entry *entry;
+ const unsigned int entry_offset=8+8*i;
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ if(entry_offset + 8 > size)
+ {
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ return ;
+ }
+ /*@ assert entry_offset + 8 <= size; */
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ entry=(const struct summary_entry *)&buffer[entry_offset];
+ OLE_parse_PropertySet_entry(buffer, size, entry, ext, title, file_time);
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ }
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
}
-static void OLE_parse_summary_aux(const unsigned char *dataPt, const unsigned int dirLen, const char **ext, char **title, time_t *file_time)
+/*@
+ @ requires 48 <= dirLen <= 1024*1024;
+ @ requires \valid_read(dataPt + (0 .. dirLen-1));
+ @ requires \initialized(dataPt + (0 .. dirLen-1));
+ @ requires \valid(ext);
+ @ requires \valid(title + (0 .. 1024-1));
+ @ requires \valid(file_time);
+ @ requires valid_string(title);
+ @ requires *ext == \null || valid_read_string(*ext);
+ @ requires separation: \separated(dataPt+(..), ext, title + (0 .. 1023), file_time);
+ @ ensures *ext == \null || valid_read_string(*ext);
+ @ ensures valid_string(title);
+ @*/
+/*X TODO assigns *ext, *(title + (0..1023)), *file_time; */
+static void OLE_parse_summary_aux(const unsigned char *dataPt, const unsigned int dirLen, const char **ext, char *title, time_t *file_time)
{
unsigned int pos;
assert(dirLen >= 48 && dirLen<=1024*1024);
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
#ifdef DEBUG_OLE
dump_log(dataPt, dirLen);
#endif
@@ -684,99 +1225,45 @@ static void OLE_parse_summary_aux(const unsigned char *dataPt, const unsigned in
return ;
pos=get32u(dataPt, 44);
if(pos > dirLen - 8)
+ {
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
return ;
+ }
+ /*@ assert pos <= dirLen - 8; */
{
-// unsigned int size;
- unsigned int numEntries;
- unsigned int i;
- numEntries=get32u(dataPt, pos+4);
-#ifdef DEBUG_OLE
+ /* PropertySet */
+ const unsigned int size=get32u(dataPt, pos);
+ if(size <= 8 || size > dirLen || pos + size > dirLen)
{
- unsigned int size=get32u(dataPt, pos);
- log_info("Property Info %u - %u at 0x%x\n", numEntries, size, pos);
- }
-#endif
- if(pos + 8 + 8 * numEntries > dirLen)
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
return ;
- for(i=0; i<numEntries; i++)
- {
- const unsigned int entry = pos + 8 + 8 * i;
- const unsigned int tag=get32u(dataPt, entry);
- const unsigned int offset=get32u(dataPt, entry + 4);
- const unsigned int valStart = pos + 4 + offset;
- unsigned int type;
- if(valStart >= dirLen)
- return ;
- type=get32u(dataPt, pos + offset);
-#ifdef DEBUG_OLE
- log_info("entry 0x%x, tag 0x%x, offset 0x%x, valStart 0x%x, type 0x%x\n",
- entry, tag, offset, valStart, type);
-#endif
- /* tag: Software, type: VT_LPSTR */
- if(tag==0x12 && type==30)
- {
- unsigned int count=get32u(dataPt, valStart);
- if(valStart + 4 + count > dirLen)
- return ;
-#ifdef DEBUG_OLE
- {
- unsigned int j;
- log_info("Software ");
- for(j=0; j<count; j++)
- {
- log_info("%c", dataPt[valStart + 4 + j]);
- }
- log_info("\n");
- }
-#endif
- software2ext(ext, count, &dataPt[valStart + 4]);
- }
- /* tag: Software, type: VT_LPWSTR */
- if(tag==0x12 && type==31)
- {
- unsigned int count=get32u(dataPt, valStart);
- if(valStart + 4 + 2 * count > dirLen)
- return ;
-#ifdef DEBUG_OLE
- {
- unsigned int j;
- log_info("Software ");
- for(j=0; j < 2 * count; j+=2)
- {
- log_info("%c", dataPt[valStart + 4 + j]);
- }
- log_info("\n");
- }
-#endif
- *ext=software_uni2ext(count, &dataPt[valStart + 4]);
- }
- if(tag==0x02 && type==30 && *title==NULL)
- {
- const unsigned int count=get32u(dataPt, valStart);
- if(valStart + 4 + count > dirLen)
- return ;
- *title=(char*)MALLOC(count+1);
- memcpy(*title, &dataPt[valStart + 4], count);
- (*title)[count]='\0';
-#ifdef DEBUG_OLE
- log_info("Title %s\n", *title);
-#endif
- }
- /* ModifyDate, type=VT_FILETIME */
- if(tag==0x0d && type==64)
- {
- uint64_t tmp=get64u(dataPt, valStart);
- tmp/=10000000;
- if(tmp > (uint64_t)134774 * 24 * 3600)
- {
- tmp -= (uint64_t)134774 * 24 * 3600;
- *file_time=tmp;
- }
- }
}
+ /*@ assert 8 < size; */
+ /*@ assert size <= dirLen; */
+ /*@ assert dirLen <=1024*1024; */
+ /*@ assert \valid_read(dataPt + (0 .. dirLen-1)); */
+ /*@ assert pos + size <= dirLen; */
+ /*@ assert \valid_read(dataPt + (0 .. pos+size-1)); */
+ /*@ assert \initialized(dataPt + (0 .. dirLen-1)); */
+ /*@ assert pos + size <= dirLen; */
+ /*X TODO assert \initialized(dataPt + (0 .. pos+size-1)); */
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ OLE_parse_PropertySet(&dataPt[pos], size, ext, title, file_time);
}
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
}
+/*@
+ @ requires \valid_read(ministream + (0 .. ministream_size-1));
+ @ requires \valid_read(minifat + (0 .. minifat_entries-1));
+ @ requires uMiniSectorShift==6;
+ @ requires 48 <= len <= 1024*1024;
+ @ ensures \result!=\null ==> \valid((char *)\result + (0 .. len-1));
+ @*/
static void *OLE_read_ministream(unsigned char *ministream,
const uint32_t *minifat, const unsigned int minifat_entries, const unsigned int uMiniSectorShift,
const unsigned int miniblock_start, const unsigned int len, const unsigned int ministream_size)
@@ -784,41 +1271,94 @@ static void *OLE_read_ministream(unsigned char *ministream,
unsigned char *dataPt;
unsigned int mblock;
unsigned int size_read;
+#ifdef __FRAMAC__
+ dataPt=(unsigned char *)MALLOC((1024*1024+(1<<uMiniSectorShift)-1) / (1<<uMiniSectorShift) * (1<<uMiniSectorShift));
+#else
dataPt=(unsigned char *)MALLOC((len+(1<<uMiniSectorShift)-1) / (1<<uMiniSectorShift) * (1<<uMiniSectorShift));
+#endif
for(mblock=miniblock_start, size_read=0;
size_read < len;
- mblock=le32(minifat[mblock]), size_read+=(1<<uMiniSectorShift))
+ size_read+=(1<<uMiniSectorShift))
{
- if(!(mblock < minifat_entries))
+ if(mblock >= minifat_entries)
{
free(dataPt);
return NULL;
}
- if((mblock<<uMiniSectorShift)+ (1<<uMiniSectorShift) <= ministream_size)
- memcpy(&dataPt[size_read], &ministream[mblock<<uMiniSectorShift], (1<<uMiniSectorShift));
+ /* TODO assert mblock < minifat_entries; */
+ if((mblock+1)> ministream_size>>uMiniSectorShift)
+ {
+ free(dataPt);
+ return NULL;
+ }
+ memcpy(&dataPt[size_read], &ministream[mblock<<uMiniSectorShift], (1<<uMiniSectorShift));
+#ifdef __FRAMAC__
+ mblock=Frama_C_interval(0, minifat_entries);
+#else
+ mblock=le32(minifat[mblock]);
+#endif
}
return dataPt;
}
+/*@
+ @ requires \valid(file);
+ @ requires \valid_read(fat + (0 .. fat_entries-1));
+ @ requires \valid_read(header);
+ @ requires 9 == le16(header->uSectorShift) || 12 == le16(header->uSectorShift);
+ @ requires 6 == le16(header->uMiniSectorShift);
+ @ requires \valid(ext);
+ @ requires \valid(title + (0 .. 1024-1));
+ @ requires \valid(file_time);
+ @ requires *ext == \null || valid_read_string(*ext);
+ @ requires valid_string(title);
+ @ requires separation: \separated(file,fat+(..), header, ext, title + (0 .. 1023), file_time);
+ @ ensures *ext == \null || valid_read_string(*ext);
+ @ ensures valid_string(title);
+ @*/
static void OLE_parse_summary(FILE *file, const uint32_t *fat, const unsigned int fat_entries,
const struct OLE_HDR *header, const unsigned int ministream_block, const unsigned int ministream_size,
- const unsigned int block, const unsigned int len, const char **ext, char **title, time_t *file_time,
+ const unsigned int block, const unsigned int len, const char **ext, char *title, time_t *file_time,
const uint64_t offset)
{
+ const unsigned int uSectorShift=le16(header->uSectorShift);
unsigned char *summary=NULL;
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
if(len < 48 || len>1024*1024)
+ {
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
return ;
+ }
+ /*@ assert 48 <= len <= 1024*1024; */
if(len < le32(header->miniSectorCutoff))
{
- if(le32(header->csectMiniFat)!=0 && ministream_size > 0 && ministream_size < 1024*1024)
+ if(le32(header->csectMiniFat)==0 || ministream_size == 0)
+ {
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ return ;
+ }
+ if(ministream_size > 1024*1024 || le32(header->csectMiniFat) > 2048)
+ {
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
+ return ;
+ }
+ /*@ assert 0 < le32(header->csectMiniFat) <= 2048; */
{
- const unsigned int mini_fat_entries=(le32(header->csectMiniFat) << le16(header->uSectorShift)) / 4;
+ const unsigned int mini_fat_entries=(le32(header->csectMiniFat) << uSectorShift) / 4;
uint32_t *minifat;
unsigned char *ministream;
if((minifat=OLE_load_MiniFAT(file, header, fat, fat_entries, offset))==NULL)
+ {
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
return ;
+ }
ministream=(unsigned char *)OLE_read_stream(file,
- fat, fat_entries, le16(header->uSectorShift),
+ fat, fat_entries, uSectorShift,
ministream_block, ministream_size, offset);
if(ministream != NULL)
{
@@ -832,27 +1372,55 @@ static void OLE_parse_summary(FILE *file, const uint32_t *fat, const unsigned in
}
else
summary=(unsigned char *)OLE_read_stream(file,
- fat, fat_entries, le16(header->uSectorShift),
+ fat, fat_entries, uSectorShift,
block, len, offset);
+#if defined(__FRAMAC__)
+ {
+ free(summary);
+ summary=MALLOC(4096);
+ Frama_C_make_unknown((char *)summary, 4096);
+ /*@ assert \initialized((char *)summary + (0 .. 4096 - 1)); */
+#if 0
+ OLE_parse_summary_aux(summary, 4096, ext, title, file_time);
+ /*@ assert valid_string(title); */
+#else
+ OLE_parse_PropertySet(summary, 4096, ext, title, file_time);
+#endif
+ /*@ assert valid_string(title); */
+ free(summary);
+ }
+#else
if(summary!=NULL)
{
OLE_parse_summary_aux(summary, len, ext, title, file_time);
free(summary);
}
+#endif
+ /*@ assert *ext == \null || valid_read_string(*ext); */
+ /*@ assert valid_string(title); */
}
+/*@
+ @ requires \valid(file_recovery);
+ @ requires valid_read_string((char*)file_recovery->filename);
+ @ requires file_recovery->file_rename==&file_rename_doc;
+ @*/
static void file_rename_doc(file_recovery_t *file_recovery)
{
const char *ext=NULL;
- char *title=NULL;
+ char title[1024];
FILE *file;
unsigned char buffer_header[512];
uint32_t *fat;
const struct OLE_HDR *header=(const struct OLE_HDR*)&buffer_header;
time_t file_time=0;
unsigned int fat_entries;
+ unsigned int uSectorShift;
+ unsigned int num_FAT_blocks;
+ title[0]='\0';
+ /*@ assert valid_string(&title[0]); */
if(strstr(file_recovery->filename, ".sdd")!=NULL)
- ext="sdd";
+ ext=extension_sdd;
if((file=fopen(file_recovery->filename, "rb"))==NULL)
return;
#ifdef DEBUG_OLE
@@ -865,10 +1433,33 @@ static void file_rename_doc(file_recovery_t *file_recovery)
fclose(file);
return ;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&buffer_header, sizeof(buffer_header));
+#endif
+ uSectorShift=le16(header->uSectorShift);
+ num_FAT_blocks=le32(header->num_FAT_blocks);
/* Sanity check */
- if(le32(header->num_FAT_blocks)==0 ||
- le32(header->num_extra_FAT_blocks)>50 ||
- le32(header->num_FAT_blocks)>109+le32(header->num_extra_FAT_blocks)*((1<<le16(header->uSectorShift))-1))
+ if( uSectorShift != 9 && uSectorShift != 12)
+ {
+ fclose(file);
+ return ;
+ }
+ /*@ assert 9 == uSectorShift || 12 == uSectorShift; */
+ if(le16(header->uMiniSectorShift) != 6)
+ {
+ fclose(file);
+ return ;
+ }
+ /* Sanity check */
+ if(num_FAT_blocks==0 ||
+ le32(header->num_extra_FAT_blocks)>50)
+ {
+ fclose(file);
+ return ;
+ }
+ /*@ assert num_FAT_blocks > 0; */
+ /*@ assert 0 <= le32(header->num_extra_FAT_blocks) <= 50; */
+ if(num_FAT_blocks > 109+le32(header->num_extra_FAT_blocks)*((1<<uSectorShift)/4-1))
{
fclose(file);
return ;
@@ -878,9 +1469,7 @@ static void file_rename_doc(file_recovery_t *file_recovery)
fclose(file);
return ;
}
- fat_entries=(le32(header->num_FAT_blocks)==0 ?
- 109:
- (le32(header->num_FAT_blocks)<<le16(header->uSectorShift))/4);
+ fat_entries=(num_FAT_blocks==0 ? 109 : (num_FAT_blocks<<uSectorShift)/4);
{
unsigned int ministream_block=0;
unsigned int ministream_size=0;
@@ -891,43 +1480,48 @@ static void file_rename_doc(file_recovery_t *file_recovery)
#ifdef DEBUG_OLE
log_info("file_rename_doc root_start_block=%u, fat_entries=%u\n", le32(header->root_start_block), fat_entries);
#endif
+#ifndef __FRAMAC__
for(block=le32(header->root_start_block), i=0;
block<fat_entries && block!=0xFFFFFFFE && i<fat_entries;
block=le32(fat[block]), i++)
+#else
+ block=le32(header->root_start_block), i=0;
+#endif
{
+ /*@ assert valid_string(&title[0]); */
struct OLE_DIR *dir_entries;
- if(my_fseek(file, (1+block)<<le16(header->uSectorShift), SEEK_SET)<0)
- {
- free(fat);
- fclose(file);
- free(title);
- return ;
- }
- dir_entries=(struct OLE_DIR *)MALLOC(1<<le16(header->uSectorShift));
- if(fread(dir_entries, 1<<le16(header->uSectorShift), 1, file)!=1)
+#ifdef __FRAMAC__
+ dir_entries=(struct OLE_DIR *)MALLOC(1<<12);
+#else
+ dir_entries=(struct OLE_DIR *)MALLOC(1<<uSectorShift);
+#endif
+ if(OLE_read_block(file, (unsigned char *)dir_entries, uSectorShift, block, 0)<0)
{
free(fat);
free(dir_entries);
fclose(file);
- free(title);
return ;
}
-
#ifdef DEBUG_OLE
log_info("Root Directory block=%u (0x%x)\n", block, block);
#endif
+ /*@ assert valid_string(&title[0]); */
{
unsigned int sid;
- const struct OLE_DIR *dir_entry=dir_entries;
+ int is_db=0;
if(i==0)
{
+ const struct OLE_DIR *dir_entry=dir_entries;
ministream_block=le32(dir_entry->start_block);
ministream_size=le32(dir_entry->size);
}
- for(sid=0, dir_entry=dir_entries;
- sid<(1<<le16(header->uSectorShift))/sizeof(struct OLE_DIR);
- sid++,dir_entry++)
+ /*@ assert valid_string(&title[0]); */
+ for(sid=0;
+ sid<(1<<uSectorShift)/sizeof(struct OLE_DIR);
+ sid++)
{
+ /*@ assert valid_string(&title[0]); */
+ const struct OLE_DIR *dir_entry=&dir_entries[sid];
if(dir_entry->type!=NO_ENTRY)
{
const char SummaryInformation[40]=
@@ -938,9 +1532,10 @@ static void file_rename_doc(file_recovery_t *file_recovery)
'r', '\0', 'm', '\0', 'a', '\0', 't', '\0',
'i', '\0', 'o', '\0', 'n', '\0', '\0', '\0'
};
+ const unsigned int namsiz=le16(dir_entry->namsiz);
#ifdef DEBUG_OLE
unsigned int j;
- for(j=0;j<64 && j<le16(dir_entry->namsiz) && dir_entry->name[j]!='\0';j+=2)
+ for(j=0;j<64 && j<namsiz && dir_entry->name[j]!='\0';j+=2)
{
log_info("%c",dir_entry->name[j]);
}
@@ -950,140 +1545,83 @@ static void file_rename_doc(file_recovery_t *file_recovery)
(unsigned int)le32(dir_entry->start_block),
(unsigned int)le32(dir_entry->size));
#endif
- switch(le16(dir_entry->namsiz))
{
- case 10:
- if(memcmp(dir_entry->name, ".\0Q\0D\0F\0\0\0",10)==0)
- ext="qdf-backup";
- break;
- case 12:
- /* 3ds max */
- if(memcmp(dir_entry->name, "S\0c\0e\0n\0e\0\0\0",12)==0)
- ext="max";
- /* Licom AlphaCAM */
- else if(memcmp(dir_entry->name,"L\0i\0c\0o\0m\0\0\0",12)==0)
- ext="amb";
+ const char *tmp=entry2ext(dir_entry);
+ /*@ assert tmp == \null || valid_read_string(tmp); */
+ if(tmp!=NULL)
+ ext=tmp;
+ /*@ assert ext == \null || valid_read_string(ext); */
+ }
+ /*@ assert valid_string(&title[0]); */
+ switch(namsiz)
+ {
+ case 4:
+ if(sid==1 && memcmp(&dir_entry->name, "1\0\0\0", 4)==0)
+ is_db=1;
+ else if(is_db==1 && sid==2 && memcmp(&dir_entry->name, "2\0\0\0", 4)==0)
+ is_db=2;
+ /*@ assert valid_string(&title[0]); */
break;
case 16:
if(sid==1 && memcmp(dir_entry->name, "d\0o\0c\0.\0d\0e\0t\0\0\0", 16)==0)
- ext="psmodel";
+ ext=extension_psmodel;
/* Windows Sticky Notes */
else if(sid==1 && memcmp(dir_entry->name, "V\0e\0r\0s\0i\0o\0n\0\0\0", 16)==0)
- ext="snt";
+ ext=extension_snt;
+ else if(is_db==1 && sid==2 && memcmp(&dir_entry->name, "C\0a\0t\0a\0l\0o\0g\0\0\0", 16)==0)
+ is_db=2;
+ /*@ assert valid_string(&title[0]); */
break;
case 18:
/* MS Excel
* Note: Microsoft Works Spreadsheet contains the same signature */
if(ext==NULL &&
memcmp(dir_entry->name, "W\0o\0r\0k\0b\0o\0o\0k\0\0\0",18)==0)
- ext="xls";
- /* Microsoft Works .wps */
- else if(memcmp(dir_entry->name,"C\0O\0N\0T\0E\0N\0T\0S\0\0\0",18)==0)
- ext="wps";
- break;
- case 20:
- /* Page Maker */
- if(memcmp(&dir_entry->name, "P\0a\0g\0e\0M\0a\0k\0e\0r\0\0\0", 20)==0)
- ext="p65";
- break;
- case 22:
- /* SigmaPlot .jnb */
- if(memcmp(dir_entry->name, "J\0N\0B\0V\0e\0r\0s\0i\0o\0n\0\0\0", 22)==0)
- ext="jnb";
- /* Autodesk Inventor part ipt or iam file */
- if(memcmp(dir_entry->name, "R\0S\0e\0S\0t\0o\0r\0a\0g\0e\0\0\0", 22)==0)
- ext="ipt";
- break;
- case 24:
- /* HP Photosmart Photo Printing Album */
- if(memcmp(dir_entry->name,"I\0m\0a\0g\0e\0s\0S\0t\0o\0r\0e\0\0\0",24)==0)
- ext="albm";
- /* Lotus Approach */
- else if(memcmp(dir_entry->name,"A\0p\0p\0r\0o\0a\0c\0h\0D\0o\0c\0\0\0",24)==0)
- ext="apr";
- break;
- case 28:
- /* Microsoft Works Spreadsheet or Chart */
- if(memcmp(dir_entry->name,"W\0k\0s\0S\0S\0W\0o\0r\0k\0B\0o\0o\0k\0\0\0",28)==0)
- ext="xlr";
- /* Visio */
- else if(memcmp(dir_entry->name,"V\0i\0s\0i\0o\0D\0o\0c\0u\0m\0e\0n\0t\0\0\0",28)==0)
- ext="vsd";
- /* SolidWorks */
- else if(memcmp(&dir_entry->name, "s\0w\0X\0m\0l\0C\0o\0n\0t\0e\0n\0t\0s\0\0\0", 28)==0)
- {
-#ifdef DJGPP
- ext="sld";
-#else
- ext="sldprt";
-#endif
- }
- break;
- case 32:
- if(memcmp(dir_entry->name, "m\0a\0n\0i\0f\0e\0s\0t\0.\0c\0a\0m\0x\0m\0l\0\0\0",32)==0)
- ext="camrec";
- break;
- case 34:
- if(memcmp(dir_entry->name, "S\0t\0a\0r\0C\0a\0l\0c\0D\0o\0c\0u\0m\0e\0n\0t\0\0\0",34)==0)
- ext="sdc";
+ ext=extension_xls;
+ /*@ assert valid_string(&title[0]); */
break;
case 36:
/* sda=StarDraw, sdd=StarImpress */
- if((ext==NULL || strcmp(ext,"sdd")!=0) &&
+ if(ext!=extension_sdd &&
memcmp(dir_entry->name, "S\0t\0a\0r\0D\0r\0a\0w\0D\0o\0c\0u\0m\0e\0n\0t\0003\0\0\0", 36)==0)
- ext="sda";
- else if(memcmp(dir_entry->name, "f\0i\0l\0e\0_\0C\0O\0M\0P\0A\0N\0Y\0_\0F\0I\0L\0E\0\0\0", 36)==0)
- ext="qbb";
- break;
- case 38:
- /* Quattro Pro spreadsheet */
- if(memcmp(dir_entry->name, "N\0a\0t\0i\0v\0e\0C\0o\0n\0t\0e\0n\0t\0_\0M\0A\0I\0N\0\0\0", 38)==0)
- ext="qpw";
- else if(memcmp(dir_entry->name, "S\0t\0a\0r\0W\0r\0i\0t\0e\0r\0D\0o\0c\0u\0m\0e\0n\0t\0\0\0", 38)==0)
- ext="sdw";
+ ext=extension_sda;
+ /*@ assert valid_string(&title[0]); */
break;
case 40:
if(memcmp(dir_entry->name, SummaryInformation, 40)==0)
{
+ /*@ assert ext == \null || valid_read_string(ext); */
+ /*@ assert valid_string(&title[0]); */
OLE_parse_summary(file, fat, fat_entries, header,
ministream_block, ministream_size,
le32(dir_entry->start_block), le32(dir_entry->size),
- &ext, &title, &file_time, 0);
+ &ext, &title[0], &file_time, 0);
+ /*@ assert valid_string(&title[0]); */
+ /*@ assert ext == \null || valid_read_string(ext); */
}
- else if(memcmp(dir_entry->name,"P\0o\0w\0e\0r\0P\0o\0i\0n\0t\0 \0D\0o\0c\0u\0m\0e\0n\0t\0\0\0", 40)==0)
- ext="ppt";
- /* Outlook */
- else if(memcmp(dir_entry->name,"_\0_\0n\0a\0m\0e\0i\0d\0_\0v\0e\0r\0s\0i\0o\0n\0001\0.\0000\0\0\0",40)==0)
- ext="msg";
+ /*@ assert valid_string(&title[0]); */
break;
- case 46:
- if(memcmp(dir_entry->name,
- "I\0S\0o\0l\0i\0d\0W\0o\0r\0k\0s\0I\0n\0f\0o\0r\0m\0a\0t\0i\0o\0n\0\0\0", 46)==0)
- {
-#ifdef DJGPP
- ext="sld";
-#else
- ext="sldprt";
-#endif
- }
- break;
- case 56:
- /* Wilcom ES Software */
- if(memcmp(dir_entry->name, WilcomDesignInformationDDD, 56)==0)
- ext="emb";
+ default:
+ /*@ assert valid_string(&title[0]); */
break;
}
- if(sid==1 && le16(dir_entry->namsiz) >=6 &&
+ /*@ assert valid_string(&title[0]); */
+ if(sid==1 && namsiz >=6 &&
memcmp(dir_entry->name, "D\0g\0n", 6)==0)
- ext="dgn";
+ ext=extension_dgn;
#ifdef DEBUG_OLE
if(ext!=NULL)
- log_info("Found %s %u\n", ext, le16(dir_entry->namsiz));
+ log_info("Found %s %u\n", ext, namsiz);
#endif
+ /*@ assert valid_string(&title[0]); */
}
+ /*@ assert valid_string(&title[0]); */
}
+ if(ext==NULL && is_db==2)
+ ext=extension_db;
}
free(dir_entries);
+ /*@ assert valid_string(&title[0]); */
}
}
free(fat);
@@ -1092,15 +1630,226 @@ static void file_rename_doc(file_recovery_t *file_recovery)
set_date(file_recovery->filename, file_time, file_time);
if(title!=NULL)
{
- file_rename(file_recovery, (const unsigned char*)title, strlen(title), 0, ext, 1);
- free(title);
+ file_rename(file_recovery, &title, strlen((const char *)title), 0, ext, 1);
}
else
file_rename(file_recovery, NULL, 0, 0, ext, 1);
}
+/*@
+ @ requires buffer_size >= sizeof(struct OLE_HDR);
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ requires separation: \separated(&file_hint_doc, buffer, file_recovery, file_recovery_new);
+ @ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_doc);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == &file_rename_doc);
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
+ @*/
+ // TODO ensures *buffer == \old(*buffer);
+ // TODO ensures *file_recovery == \old(*file_recovery);
+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)
+{
+ /*@ assert file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename); */
+ const struct OLE_HDR *header=(const struct OLE_HDR *)buffer;
+ /* Check for Little Endian */
+ if(le16(header->uByteOrder)!=0xFFFE)
+ return 0;
+ if(le16(header->uDllVersion)!=3 && le16(header->uDllVersion)!=4)
+ return 0;
+ if(le16(header->reserved)!=0 || le32(header->reserved1)!=0)
+ return 0;
+ if(le16(header->uMiniSectorShift)!=6)
+ return 0;
+ if(le16(header->uDllVersion)==3 && le16(header->uSectorShift)!=9)
+ return 0;
+ /* max and qbb file have uSectorShift=12 */
+ if(le16(header->uDllVersion)==4 && le16(header->uSectorShift)!=12)
+ return 0;
+ if(le16(header->uDllVersion)==3 && le32(header->csectDir)!=0)
+ return 0;
+ /* max file have csectDir=1
+ * qbb file have csectDir=4 */
+ if(le16(header->uDllVersion)==4 && le32(header->csectDir)==0)
+ return 0;
+ /*
+ num_FAT_blocks=109+num_extra_FAT_blocks*(512-1);
+ maximum file size is 512+(num_FAT_blocks*128)*512, about 1.6GB
+ */
+ if(le32(header->num_FAT_blocks)==0 ||
+ le32(header->num_extra_FAT_blocks)>50 ||
+ le32(header->num_FAT_blocks)>109+le32(header->num_extra_FAT_blocks)*((1<<le16(header->uSectorShift))/4-1))
+ return 0;
+ /*@ assert file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename); */
+ /*@ assert le32(header->num_FAT_blocks) <= 109+le32(header->num_extra_FAT_blocks)*((1<<le16(header->uSectorShift))/4-1); */
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->file_check=&file_check_doc;
+ file_recovery_new->file_rename=&file_rename_doc;
+ file_recovery_new->extension=ole_get_file_extension(header, buffer_size);
+ if(file_recovery_new->extension!=NULL)
+ {
+ /*@ assert valid_read_string(file_recovery_new->extension); */
+ if(strcmp(file_recovery_new->extension,"sda")==0)
+ {
+ if(td_memmem(buffer,buffer_size,"StarImpress",11)!=NULL)
+ file_recovery_new->extension=extension_sdd;
+ }
+ else if(strcmp(file_recovery_new->extension,"wps")==0)
+ {
+ /* Distinguish between MS Works .wps and MS Publisher .pub */
+ if(td_memmem(buffer,buffer_size,"Microsoft Publisher",19)!=NULL)
+ file_recovery_new->extension=extension_pub;
+ }
+ /*@ assert valid_read_string(file_recovery_new->extension); */
+ return 1;
+ }
+ if(td_memmem(buffer,buffer_size,"WordDocument",12)!=NULL)
+ {
+ file_recovery_new->extension=file_hint_doc.extension;
+ }
+ else if(td_memmem(buffer,buffer_size,"StarDraw",8)!=NULL)
+ {
+ file_recovery_new->extension=extension_sda;
+ }
+ else if(td_memmem(buffer,buffer_size,"StarCalc",8)!=NULL)
+ {
+ file_recovery_new->extension=extension_sdc;
+ }
+ else if(td_memmem(buffer,buffer_size,"StarImpress",11)!=NULL)
+ {
+ file_recovery_new->extension=extension_sdd;
+ }
+ else if(td_memmem(buffer,buffer_size,"Worksheet",9)!=NULL ||
+ td_memmem(buffer,buffer_size,"Book",4)!=NULL ||
+ td_memmem(buffer,buffer_size,"Workbook",8)!=NULL ||
+ td_memmem(buffer,buffer_size,"Calc",4)!=NULL)
+ {
+ file_recovery_new->extension=extension_xls;
+ }
+ else if(td_memmem(buffer,buffer_size,"Power",5)!=NULL)
+ {
+ file_recovery_new->extension=extension_ppt;
+ }
+ else if(td_memmem(buffer,buffer_size,"AccessObjSiteData",17)!=NULL)
+ {
+ file_recovery_new->extension=extension_mdb;
+ }
+ else if(td_memmem(buffer,buffer_size,"Visio",5)!=NULL)
+ {
+ file_recovery_new->extension=extension_vsd;
+ }
+ else if(td_memmem(buffer,buffer_size,"SfxDocument",11)!=NULL)
+ {
+ file_recovery_new->extension=extension_sdw;
+ }
+ else if(td_memmem(buffer,buffer_size,"CPicPage",8)!=NULL)
+ { /* Flash Project File */
+ file_recovery_new->extension=extension_fla;
+ }
+ else if(td_memmem(buffer,buffer_size,"Microsoft Publisher",19)!=NULL)
+ { /* Publisher */
+ file_recovery_new->extension=extension_pub;
+ }
+ else if(td_memmem(buffer, buffer_size, "Microsoft Works Database", 24)!=NULL
+ || td_memmem( buffer, buffer_size, "MSWorksDBDoc", 12)!=NULL)
+ { /* Microsoft Works .wdb */
+ file_recovery_new->extension=extension_wdb;
+ }
+ else if(td_memmem(buffer,buffer_size,"MetaStock",9)!=NULL)
+ { /* MetaStock */
+ file_recovery_new->extension=extension_mws;
+ }
+ else
+ file_recovery_new->extension=file_hint_doc.extension;
+ /*@ assert valid_read_string(file_recovery_new->extension); */
+ return 1;
+}
+
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_doc(file_stat_t *file_stat)
{
static const unsigned char doc_header[]= { 0xd0, 0xcf, 0x11, 0xe0, 0xa1, 0xb1, 0x1a, 0xe1};
register_header_check(0, doc_header,sizeof(doc_header), &header_check_doc, file_stat);
}
+
+#if defined(MAIN_doc)
+#define BLOCKSIZE 65536u
+int main()
+{
+ const char fn[] = "recup_dir.1/f0000000.doc";
+ unsigned char buffer[BLOCKSIZE];
+ file_recovery_t file_recovery_new;
+ file_recovery_t file_recovery;
+ file_stat_t file_stats;
+
+ /*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+
+ reset_file_recovery(&file_recovery);
+ file_recovery.blocksize=BLOCKSIZE;
+ file_recovery_new.blocksize=BLOCKSIZE;
+ file_recovery_new.data_check=NULL;
+ file_recovery_new.file_stat=NULL;
+ file_recovery_new.file_check=NULL;
+ file_recovery_new.file_rename=NULL;
+ file_recovery_new.calculated_file_size=0;
+ file_recovery_new.file_size=0;
+ file_recovery_new.location.start=0;
+
+ file_stats.file_hint=&file_hint_doc;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ register_header_check_doc(&file_stats);
+ if(header_check_doc(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.file_check == &file_check_doc; */
+ /*@ assert file_recovery_new.file_rename == &file_rename_doc; */
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ /*@ assert \separated(&file_recovery_new, file_recovery_new.extension); */
+#ifdef __FRAMAC__
+ file_recovery_new.file_size = 512*Frama_C_interval(1, 1000);
+#endif
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ /*@ assert valid_read_string((char *)&file_recovery_new.filename); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*X TODO assert valid_read_string(file_recovery_new.extension); */
+ file_recovery_new.file_stat=&file_stats;
+ if(file_recovery_new.file_stat!=NULL)
+ {
+ file_recovery_t file_recovery_new2;
+ /* Test when another file of the same is detected in the next block */
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+ header_check_doc(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ {
+ file_recovery_new.handle=fopen(fn, "rb");
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_doc(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_rename_doc(&file_recovery_new);
+ return 0;
+}
+#endif