summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-01-18 10:40:59 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2020-01-18 10:40:59 +0100
commit4df871bf15bd29319eeb127af798ebe13c0ffc5a (patch)
tree57ec4575ad442c76fa61527eccbec11746200716
parent9b51c2aeb03fe414b7946043ad39e7ab0b1d0cf9 (diff)
PhotoRec: add a few frama-c annotations, mostly in header_check functions
-rw-r--r--src/file_bmp.c3
-rw-r--r--src/file_doc.c2
-rw-r--r--src/file_emf.c10
-rw-r--r--src/file_exe.c8
-rw-r--r--src/file_gpg.c12
-rw-r--r--src/file_mov.c5
-rw-r--r--src/file_mp3.c18
-rw-r--r--src/file_pf.c11
-rw-r--r--src/file_spe.c3
-rw-r--r--src/file_txt.c39
-rw-r--r--src/file_zip.c10
-rw-r--r--src/filegen.c3
-rw-r--r--src/filegen.h3
13 files changed, 115 insertions, 12 deletions
diff --git a/src/file_bmp.c b/src/file_bmp.c
index 2effbe9..090f538 100644
--- a/src/file_bmp.c
+++ b/src/file_bmp.c
@@ -88,12 +88,15 @@ struct bmp_header
@ 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) ==> \initialized(&file_recovery_new->time);
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_bmp.extension);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 65);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 65);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
@ ensures *buffer==\old(*buffer);
diff --git a/src/file_doc.c b/src/file_doc.c
index b1cd178..4c25d08 100644
--- a/src/file_doc.c
+++ b/src/file_doc.c
@@ -1647,6 +1647,8 @@ static void file_rename_doc(file_recovery_t *file_recovery)
@ 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->time == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ 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);
diff --git a/src/file_emf.c b/src/file_emf.c
index 1db17a8..b4a10d0 100644
--- a/src/file_emf.c
+++ b/src/file_emf.c
@@ -368,19 +368,23 @@ static data_check_t data_check_emf(const unsigned char *buffer, const unsigned i
}
/*@
- @ requires buffer_size >= sizeof(struct EMF_HDR);
+ @ requires buffer_size > 0;
@ 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_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->extension == file_hint_emf.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 0x34);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
- @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_emf);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
@@ -390,6 +394,8 @@ static int header_check_emf(const unsigned char *buffer, const unsigned int buff
static const unsigned char emf_header[4]= { 0x01, 0x00, 0x00, 0x00};
const struct EMF_HDR *hdr=(const struct EMF_HDR *)buffer;
const unsigned int atom_size=le32(hdr->emr.nSize);
+ if(buffer_size < sizeof(struct EMF_HDR))
+ return 0;
if(memcmp(buffer,emf_header,sizeof(emf_header))==0 &&
le32(hdr->nBytes) >= 88 &&
le16(hdr->sReserved)==0 &&
diff --git a/src/file_exe.c b/src/file_exe.c
index 465fab2..2050e21 100644
--- a/src/file_exe.c
+++ b/src/file_exe.c
@@ -58,11 +58,19 @@ static const unsigned char exe_header[2] = {'M','Z'};
@ requires buffer_size >= 2;
@ 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_exe, 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->extension == file_hint_exe.extension || file_recovery_new->extension == extension_dll);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null || file_recovery_new->data_check == &data_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == \null || file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null || file_recovery_new->file_rename == &file_rename_pe_exe);
+ @ 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_exe(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)
{
diff --git a/src/file_gpg.c b/src/file_gpg.c
index ac700e2..ec9635e 100644
--- a/src/file_gpg.c
+++ b/src/file_gpg.c
@@ -474,8 +474,18 @@ static void file_check_gpg(file_recovery_t *file_recovery)
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(file_recovery, file_recovery_new);
@ ensures \result == 0 || \result == 1;
- @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_gpg);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_gpg.extension || file_recovery_new->extension == extension_pgp);
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_gpg);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
+ @ 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_gpg(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)
{
diff --git a/src/file_mov.c b/src/file_mov.c
index b330395..a403eb9 100644
--- a/src/file_mov.c
+++ b/src/file_mov.c
@@ -201,10 +201,13 @@ static data_check_t data_check_mov(const unsigned char *buffer, const unsigned i
@ requires buffer_size >= 16;
@ 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_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->extension == file_hint_mov.extension ||
file_recovery_new->extension == extension_3g2 ||
file_recovery_new->extension == extension_3gp ||
@@ -213,12 +216,14 @@ static data_check_t data_check_mov(const unsigned char *buffer, const unsigned i
file_recovery_new->extension == extension_jp2 ||
file_recovery_new->extension == extension_m4p ||
file_recovery_new->extension == extension_mp4);
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@ ensures (\result == 1) ==> (file_recovery_new->file_rename == &file_rename_mov || file_recovery_new->file_rename == \null);
@ ensures (\result == 1 && file_recovery_new->extension == file_hint_mov.extension) ==> (file_recovery_new->file_rename == file_rename_mov);
@ ensures (\result == 1 && file_recovery_new->extension != file_hint_mov.extension) ==> (file_recovery_new->file_rename == \null);
@ ensures (\result == 1 && (file_recovery_new->extension == extension_jp2 || file_recovery_new->blocksize < 16)) ==> (file_recovery_new->data_check == \null && file_recovery_new->file_check == \null && file_recovery_new->file_rename == \null && file_recovery_new->min_filesize > 0);
@ ensures (\result == 1 && file_recovery_new->extension != extension_jp2 && file_recovery_new->blocksize >= 16) ==> (file_recovery_new->calculated_file_size > 0 && file_recovery_new->file_check == &file_check_size && file_recovery_new->data_check == &data_check_mov);
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
@*/
static int header_check_mov_aux(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)
{
diff --git a/src/file_mp3.c b/src/file_mp3.c
index b159e31..fb311ed 100644
--- a/src/file_mp3.c
+++ b/src/file_mp3.c
@@ -440,16 +440,20 @@ static data_check_t data_check_id3(const unsigned char *buffer, const unsigned i
@ requires buffer_size >= 10;
@ 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_recovery, file_recovery_new);
+ @ requires separation: \separated(&file_hint_mp3, 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->extension == file_hint_mp3.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size > 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 287);
- @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_id3);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
@@ -489,18 +493,22 @@ static int header_check_id3(const unsigned char *buffer, const unsigned int buff
@ requires buffer_size >= 6;
@ 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_recovery, file_recovery_new);
+ @ requires separation: \separated(&file_hint_mp3, 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->extension == file_hint_mp3.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size > 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 287);
- @ ensures (\result == 1 && file_recovery_new->blocksize >= 16) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1 && file_recovery_new->blocksize >= 16) ==> (file_recovery_new->data_check == &data_check_mp3);
- @ ensures (\result == 1 && file_recovery_new->blocksize < 16) ==> (file_recovery_new->file_check == \null);
+ @ ensures (\result == 1 && file_recovery_new->blocksize >= 16) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1 && file_recovery_new->blocksize < 16) ==> (file_recovery_new->data_check == \null);
+ @ ensures (\result == 1 && file_recovery_new->blocksize < 16) ==> (file_recovery_new->file_check == \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
diff --git a/src/file_pf.c b/src/file_pf.c
index bff762b..d01b99d 100644
--- a/src/file_pf.c
+++ b/src/file_pf.c
@@ -90,13 +90,20 @@ static void file_rename_pf(file_recovery_t *file_recovery)
@ requires \valid_read(file_recovery);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
- @ requires separation: \separated(file_recovery, file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ requires separation: \separated(&file_hint_pf, 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->extension == file_hint_pf.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= sizeof(struct pf_header));
- @ ensures (\result == 1) ==> (file_recovery_new->file_rename==&file_rename_pf);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check==&data_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_check==&file_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename==&file_rename_pf);
+ @ 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_pf(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)
{
diff --git a/src/file_spe.c b/src/file_spe.c
index d276953..0e79aab 100644
--- a/src/file_spe.c
+++ b/src/file_spe.c
@@ -36,7 +36,6 @@
#endif
static void register_header_check_spe(file_stat_t *file_stat);
-static int header_check_spe(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);
const file_hint_t file_hint_spe= {
.extension="spe",
@@ -251,11 +250,13 @@ struct header_spe
@ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
@ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_spe.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 4100);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 4100);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
@ assigns file_recovery_new->filename[0];
diff --git a/src/file_txt.c b/src/file_txt.c
index d009e1e..aec7b7f 100644
--- a/src/file_txt.c
+++ b/src/file_txt.c
@@ -1048,6 +1048,7 @@ static void file_check_xml(file_recovery_t *file_recovery)
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_dc);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
@@ -1085,6 +1086,7 @@ static int header_check_dc(const unsigned char *buffer, const unsigned int buffe
@ ensures file_recovery_new->calculated_file_size == 0;
@ ensures file_recovery_new->extension == extension_ers;
@ ensures file_recovery_new->file_size == 0;
+ @ ensures file_recovery_new->min_filesize == 0;
@ ensures file_recovery_new->data_check == &data_check_txt;
@ ensures file_recovery_new->file_check == &file_check_ers;
@ ensures file_recovery_new->file_rename == \null;
@@ -1114,6 +1116,7 @@ static int header_check_ers(const unsigned char *buffer, const unsigned int buff
@ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
@ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize > 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@@ -1140,6 +1143,7 @@ static int header_check_fasttxt(const unsigned char *buffer, const unsigned int
file_recovery_new->min_filesize=header->len+1;
/*@ assert file_recovery_new->file_stat == \null; */
/*@ assert file_recovery_new->handle == \null; */
+ /*@ assert file_recovery_new->min_filesize > 0; */
/*@ assert file_recovery_new->calculated_file_size == 0; */
/*@ assert file_recovery_new->file_size == 0; */
/*@ assert file_recovery_new->data_check == &data_check_txt; */
@@ -1167,6 +1171,7 @@ static int header_check_fasttxt(const unsigned char *buffer, const unsigned int
@ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_html);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_html);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@@ -1208,6 +1213,7 @@ static int header_check_html(const unsigned char *buffer, const unsigned int buf
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_ics);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -1286,6 +1292,7 @@ static int header_check_le16_txt(const unsigned char *buffer, const unsigned int
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_mbox);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -1325,6 +1332,7 @@ static int header_check_mbox(const unsigned char *buffer, const unsigned int buf
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -1335,6 +1343,7 @@ static int header_check_mbox(const unsigned char *buffer, const unsigned int buf
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_java || file_recovery_new->extension == extension_pm);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -1371,6 +1380,7 @@ static int header_check_perlm(const unsigned char *buffer, const unsigned int bu
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -1381,6 +1391,7 @@ static int header_check_perlm(const unsigned char *buffer, const unsigned int bu
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_rtf);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -1413,6 +1424,7 @@ static int header_check_rtf(const unsigned char *buffer, const unsigned int buff
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -1423,6 +1435,7 @@ static int header_check_rtf(const unsigned char *buffer, const unsigned int buff
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_smil);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_smil);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -1443,6 +1456,7 @@ static int header_check_smil(const unsigned char *buffer, const unsigned int buf
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -1476,6 +1490,7 @@ static int header_check_snz(const unsigned char *buffer, const unsigned int buff
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -1486,6 +1501,7 @@ static int header_check_snz(const unsigned char *buffer, const unsigned int buff
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_stl);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -1509,6 +1525,7 @@ static int header_check_stl(const unsigned char *buffer, const unsigned int buff
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -1519,6 +1536,7 @@ static int header_check_stl(const unsigned char *buffer, const unsigned int buff
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_svg);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_svg);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -1547,6 +1565,7 @@ static int header_check_svg(const unsigned char *buffer, const unsigned int buff
@ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_mbox);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@@ -1576,6 +1595,7 @@ static int header_check_thunderbird(const unsigned char *buffer, const unsigned
/*@
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -1586,6 +1606,7 @@ static int header_check_thunderbird(const unsigned char *buffer, const unsigned
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_ttd);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_ttd);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -1618,6 +1639,7 @@ static int header_check_ttd(const unsigned char *buffer, const unsigned int buff
@ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
@ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == \null || file_recovery_new->data_check == &data_check_html || file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_emlx || file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null || file_recovery_new->file_rename == &file_rename_html);
@@ -1950,6 +1972,7 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -1960,6 +1983,7 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_vbm);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_vbm);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -1978,6 +2002,7 @@ static int header_check_vbm(const unsigned char *buffer, const unsigned int buff
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -1987,6 +2012,7 @@ static int header_check_vbm(const unsigned char *buffer, const unsigned int buff
@ ensures file_recovery_new->handle == \null;
@ ensures file_recovery_new->calculated_file_size == 0;
@ ensures file_recovery_new->file_size == 0;
+ @ ensures file_recovery_new->min_filesize == 0;
@ ensures file_recovery_new->data_check == \null ||
file_recovery_new->data_check == data_check_html ||
file_recovery_new->data_check == data_check_txt;
@@ -2110,6 +2136,7 @@ static int header_check_xml(const unsigned char *buffer, const unsigned int buff
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -2120,6 +2147,7 @@ static int header_check_xml(const unsigned char *buffer, const unsigned int buff
@ ensures file_recovery_new->extension == extension_ghx || file_recovery_new->extension == extension_xml;
@ ensures file_recovery_new->calculated_file_size == 0;
@ ensures file_recovery_new->file_size == 0;
+ @ ensures file_recovery_new->min_filesize == 0;
@ ensures (buffer_size >= 10) ==> (file_recovery_new->data_check == &data_check_xml_utf8);
@ ensures (buffer_size < 10) ==> file_recovery_new->data_check == \null;
@ ensures file_recovery_new->file_check == &file_check_xml;
@@ -2164,6 +2192,7 @@ static int header_check_xml_utf8(const unsigned char *buffer, const unsigned int
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -2174,6 +2203,7 @@ static int header_check_xml_utf8(const unsigned char *buffer, const unsigned int
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_xml);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == \null);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -2197,6 +2227,7 @@ static int header_check_xml_utf16(const unsigned char *buffer, const unsigned in
@ requires buffer_size > 0;
@ 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->extension);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@@ -2207,6 +2238,7 @@ static int header_check_xml_utf16(const unsigned char *buffer, const unsigned in
@ ensures (\result == 1) ==> (file_recovery_new->extension == extension_xmp);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
@@ -2886,6 +2918,7 @@ static int main_perlm()
file_recovery.blocksize=BLOCKSIZE;
file_recovery_new.blocksize=BLOCKSIZE;
file_recovery_new.data_check=NULL;
+ file_recovery_new.extension=NULL;
file_recovery_new.file_stat=NULL;
file_recovery_new.file_check=NULL;
file_recovery_new.file_rename=NULL;
@@ -2906,6 +2939,7 @@ static int main_perlm()
file_recovery_new.file_stat=&file_stats;
/*@ assert valid_read_string((char *)file_recovery_new.filename); */
/*@ assert file_recovery_new.extension == extension_pm || file_recovery_new.extension == extension_java; */
+ /*@ assert valid_read_string((char *)file_recovery_new.extension); */
/*@ assert file_recovery_new.calculated_file_size == 0; */
/*@ assert file_recovery_new.file_size == 0; */
/*@ assert file_recovery_new.data_check == &data_check_txt; */
@@ -2973,6 +3007,7 @@ static int main_rtf()
file_recovery.blocksize=BLOCKSIZE;
file_recovery_new.blocksize=BLOCKSIZE;
file_recovery_new.data_check=NULL;
+ file_recovery_new.extension=NULL;
file_recovery_new.file_stat=NULL;
file_recovery_new.file_check=NULL;
file_recovery_new.file_rename=NULL;
@@ -3147,6 +3182,7 @@ static int main_snz()
file_recovery.blocksize=BLOCKSIZE;
file_recovery_new.blocksize=BLOCKSIZE;
file_recovery_new.data_check=NULL;
+ file_recovery_new.extension=NULL;
file_recovery_new.file_stat=NULL;
file_recovery_new.file_check=NULL;
file_recovery_new.file_rename=NULL;
@@ -3234,6 +3270,7 @@ static int main_stl()
file_recovery.blocksize=BLOCKSIZE;
file_recovery_new.blocksize=BLOCKSIZE;
file_recovery_new.data_check=NULL;
+ file_recovery_new.extension=NULL;
file_recovery_new.file_stat=NULL;
file_recovery_new.file_check=NULL;
file_recovery_new.file_rename=NULL;
@@ -3473,6 +3510,7 @@ static int main_ttd()
file_recovery.blocksize=BLOCKSIZE;
file_recovery_new.blocksize=BLOCKSIZE;
file_recovery_new.data_check=NULL;
+ file_recovery_new.extension=NULL;
file_recovery_new.file_stat=NULL;
file_recovery_new.file_check=NULL;
file_recovery_new.file_rename=NULL;
@@ -3987,6 +4025,7 @@ static int main_xmp()
file_recovery.blocksize=BLOCKSIZE;
file_recovery_new.blocksize=BLOCKSIZE;
file_recovery_new.data_check=NULL;
+ file_recovery_new.extension=NULL;
file_recovery_new.file_stat=NULL;
file_recovery_new.file_check=NULL;
file_recovery_new.file_rename=NULL;
diff --git a/src/file_zip.c b/src/file_zip.c
index c674b2f..f80d461 100644
--- a/src/file_zip.c
+++ b/src/file_zip.c
@@ -980,14 +980,23 @@ static void file_rename_zip(file_recovery_t *file_recovery)
@ requires buffer_size >= 85;
@ 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->extension);
@ 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_zip, 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->time == 0);
@ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 21);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_zip || file_recovery_new->file_check == \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename == &file_rename_zip || file_recovery_new->file_rename == \null);
+ @ 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_zip(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)
{
@@ -1154,6 +1163,7 @@ int main()
file_recovery.blocksize=BLOCKSIZE;
file_recovery_new.blocksize=BLOCKSIZE;
file_recovery_new.data_check=NULL;
+ file_recovery_new.extension=NULL;
file_recovery_new.file_stat=NULL;
file_recovery_new.file_check=NULL;
file_recovery_new.file_rename=NULL;
diff --git a/src/filegen.c b/src/filegen.c
index 93912c1..db9fca9 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -722,6 +722,9 @@ int file_rename_unicode(file_recovery_t *file_recovery, const void *buffer, cons
static uint64_t offset_skipped_header=0;
+/*@
+ @ assigns offset_skipped_header;
+ @*/
void header_ignored_cond_reset(uint64_t start, uint64_t end)
{
if(start <= offset_skipped_header && offset_skipped_header <= end)
diff --git a/src/filegen.h b/src/filegen.h
index a7ebde4..2c6af8a 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -149,8 +149,9 @@ void file_search_footer(file_recovery_t *file_recovery, const void*footer, const
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check == &data_check_size;
- @ assigns \nothing;
@ ensures \result == DC_STOP || \result == DC_CONTINUE;
+ @ ensures file_recovery->data_check == &data_check_size;
+ @ assigns \nothing;
@*/
data_check_t data_check_size(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);