summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-11-16 09:36:00 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-11-16 09:36:00 +0100
commit90efd3e667ab7be0f04e0749903571305756bd0c (patch)
tree0e6d17b9d82d67637e6d5b90f9c837c9512423e8
parent8e0867ad23529c4695e4c585d0651e3ac148b8de (diff)
src/file_doc.c: additional frama-c checks, minor patch for
ole_get_file_extension()
-rw-r--r--src/file_doc.c36
1 files changed, 27 insertions, 9 deletions
diff --git a/src/file_doc.c b/src/file_doc.c
index 4c28452..67b24ac 100644
--- a/src/file_doc.c
+++ b/src/file_doc.c
@@ -307,13 +307,23 @@ static const char *ole_get_file_extension(const struct OLE_HDR *header, const un
if(tmp!=NULL)
return tmp;
}
- 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 ||
- memcmp(&dir_entry->name, "C\0a\0t\0a\0l\0o\0g\0", 14)==0))
- is_db=2;
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 */
@@ -331,7 +341,7 @@ static const char *ole_get_file_extension(const struct OLE_HDR *header, const un
}
if(ext!=NULL)
{
- /*@ assert ext == extension_xls; */
+ /*@ assert ext == extension_xls || ext == extension_psmodel || ext == extension_snt; */
return ext;
}
/* Thumbs.db */
@@ -428,6 +438,7 @@ static uint32_t *OLE_load_FAT(FILE *IN, const struct OLE_HDR *header, const uint
/*@
@ 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)
{
@@ -584,6 +595,7 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
/*@
@ requires \valid(file_recovery);
@ requires \valid(file_recovery->handle);
+ @ ensures \valid(file_recovery->handle);
@*/
static void file_check_doc(file_recovery_t *file_recovery)
{
@@ -1415,7 +1427,7 @@ static void file_rename_doc(file_recovery_t *file_recovery)
case 4:
if(sid==1 && memcmp(&dir_entry->name, "1\0\0\0", 4)==0)
is_db=1;
- if(is_db==1 && sid==2 && memcmp(&dir_entry->name, "2\0\0\0", 4)==0)
+ else if(is_db==1 && sid==2 && memcmp(&dir_entry->name, "2\0\0\0", 4)==0)
is_db=2;
break;
case 16:
@@ -1485,11 +1497,15 @@ static void file_rename_doc(file_recovery_t *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_recovery, file_recovery_new);
+ @ 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) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
@*/
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)
{
@@ -1652,6 +1668,8 @@ int main()
/*@ 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