summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-09-12 16:19:07 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-09-12 16:19:07 +0200
commit12bb2ea5ae3f35dcc8c472d87d9319f8443b37df (patch)
treefe9969c0d10793bd41e78d1b5e3fb33979b60b97
parenta7606a61fcf52be87294d4552618567fd7f2749c (diff)
PhotoRec: fix problems reported by frama-c
-rw-r--r--src/file_bkf.c50
-rw-r--r--src/filegen.c33
-rw-r--r--src/filegen.h13
3 files changed, 74 insertions, 22 deletions
diff --git a/src/file_bkf.c b/src/file_bkf.c
index b509dd2..5aac25c 100644
--- a/src/file_bkf.c
+++ b/src/file_bkf.c
@@ -33,12 +33,15 @@
#include "common.h"
#include "log.h"
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_bkf(file_stat_t *file_stat);
const file_hint_t file_hint_bkf= {
.extension="bkf",
.description="MS Backup file",
- .max_filesize=-1,
+ .max_filesize=PHOTOREC_MAX_FILE_SIZE,
.recover=1,
.enable_by_default=1,
.register_header_check=&register_header_check_bkf
@@ -63,12 +66,57 @@ struct mtf_db_hdr
uint16_t check; /* header checksum */
} __attribute__ ((gcc_struct, __packed__));
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires \valid_read(&file_recovery->extension);
+ @ requires valid_read_string(file_recovery->extension);
+ @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
+ @ requires \initialized(&file_recovery->time);
+ @
+ @ requires file_recovery->file_check == &file_check_bkf;
+ @ assigns *file_recovery->handle, errno, file_recovery->file_size;
+ @ assigns Frama_C_entropy_source;
+ @
+ @ ensures \valid(file_recovery->handle);
+ @*/
static void file_check_bkf(file_recovery_t *file_recovery)
{
const unsigned char bkf_footer[4]= { 'S', 'F', 'M', 'B'};
file_search_footer(file_recovery, bkf_footer, sizeof(bkf_footer), 0x400-4);
}
+/*@
+ @ 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 buffer_size >= sizeof(struct mtf_db_hdr);
+ @ requires separation: \separated(&file_hint_bkf, 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) ==> \initialized(&file_recovery_new->time);
+ @ ensures (\result == 1) ==> \initialized(&file_recovery_new->calculated_file_size);
+ @ ensures (\result == 1) ==> file_recovery_new->file_size == 0;
+ @ ensures (\result == 1) ==> \initialized(&file_recovery_new->min_filesize);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null || \valid_function(file_recovery_new->data_check));
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == \null || \valid_function(file_recovery_new->file_check));
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null || \valid_function(file_recovery_new->file_rename));
+ @ ensures (\result != 0) ==> file_recovery_new->extension != \null;
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->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->min_filesize == 52);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_bkf.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_bkf);
+ @*/
static int header_check_bkf(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 struct mtf_db_hdr *hdr=(const struct mtf_db_hdr *)buffer;
diff --git a/src/filegen.c b/src/filegen.c
index 16b6a25..751b78f 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -45,9 +45,6 @@
#include "common.h"
#include "filegen.h"
#include "log.h"
-#if defined(__FRAMAC__)
-#include "__fc_builtin.h"
-#endif
static file_check_t file_check_plist={
.list = TD_LIST_HEAD_INIT(file_check_plist.list)
@@ -275,16 +272,19 @@ void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode)
uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const unsigned int footer_length)
{
- unsigned char*buffer;
- assert(footer_length < 4096);
- /*@ assert 0 < footer_length < 4096; */
/*
* 4096+footer_length-1: required size
* 4096+footer_length: to avoid a Frama-C warning when footer_length==1
* 8192: maximum size
* */
- buffer=(unsigned char*)MALLOC(4096+footer_length);
- memset(buffer+4096,0,footer_length-1);
+ char buffer[8192];
+ assert(footer_length < 4096);
+ /*@ assert 0 < footer_length < 4096; */
+ memset(&buffer[4096],0,footer_length-1);
+ /*@
+ @ loop assigns errno, *handle, Frama_C_entropy_source;
+ @ loop assigns offset, buffer[0 .. 8192-1];
+ @*/
do
{
int i;
@@ -296,27 +296,24 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
else
offset=offset-(offset%4096);
if(my_fseek(handle,offset,SEEK_SET)<0)
- {
- free(buffer);
return 0;
- }
- taille=fread(buffer, 1, 4096, handle);
+ taille=fread(&buffer, 1, 4096, handle);
if(taille <= 0)
- {
- free(buffer);
return 0;
- }
+ /*@ assert 0 < taille <= 4096; */
+#ifdef __FRAMAC__
+ Frama_C_make_unknown(&buffer, 4096);
+#endif
+ /*@ loop assigns i; */
for(i=taille-1;i>=0;i--)
{
- if(buffer[i]==*(const unsigned char *)footer && memcmp(buffer+i,footer,footer_length)==0)
+ if(buffer[i]==*(const char *)footer && memcmp(&buffer[i],footer,footer_length)==0)
{
- free(buffer);
return offset + i;
}
}
memcpy(buffer+4096,buffer,footer_length-1);
} while(offset>0);
- free(buffer);
return 0;
}
diff --git a/src/filegen.h b/src/filegen.h
index cfd9a72..6dc76b4 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -24,6 +24,9 @@
#ifdef __cplusplus
extern "C" {
#endif
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
#include "list.h"
@@ -130,18 +133,22 @@ void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode);
/*@
@ requires \valid(handle);
- @ requires footer_length > 0;
+ @ requires 0 < footer_length < 4096;
@ requires \valid_read((char *)footer+(0..footer_length-1));
+ @ requires \separated(handle, (char *)footer + (..), &errno, &Frama_C_entropy_source);
+ @ assigns *handle, errno, Frama_C_entropy_source;
@*/
uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const unsigned int footer_length);
/*@
@ requires \valid(file_recovery);
@ requires \valid(file_recovery->handle);
- @ requires footer_length > 0;
+ @ requires 0 < footer_length < 4096;
@ requires \valid_read((char *)footer+(0..footer_length-1));
- @ requires \separated(file_recovery, file_recovery->handle);
+ @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
@ ensures \valid(file_recovery->handle);
+ @ assigns *file_recovery->handle, errno, file_recovery->file_size;
+ @ assigns Frama_C_entropy_source;
@*/
void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length);