summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-09-13 15:35:44 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-09-13 15:35:44 +0200
commitb478a161acc8cb39c10c7cf9040a49b8d86c2b64 (patch)
tree87e6baaa5bce09b4838b654763a1cac543a8090a
parent57215f88564f676e8f315fc14985da8b88733371 (diff)
PhotoRec: src/file_fcs.c - fix problems reported by frama-c
-rw-r--r--src/file_fcs.c85
1 files changed, 76 insertions, 9 deletions
diff --git a/src/file_fcs.c b/src/file_fcs.c
index 1ad1af9..58c5a26 100644
--- a/src/file_fcs.c
+++ b/src/file_fcs.c
@@ -32,8 +32,10 @@
#include "filegen.h"
#include "log.h"
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_fcs(file_stat_t *file_stat);
-static int header_check_fcs(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_fcs= {
.extension="fcs",
@@ -44,13 +46,6 @@ const file_hint_t file_hint_fcs= {
.register_header_check=&register_header_check_fcs
};
-static const unsigned char fcs_signature[6]= {'F','C','S','3','.','0'};
-
-static void register_header_check_fcs(file_stat_t *file_stat)
-{
- register_header_check(0, fcs_signature, sizeof(fcs_signature), &header_check_fcs, file_stat);
-}
-
struct fcs_header
{
unsigned char magic[6];
@@ -63,36 +58,95 @@ struct fcs_header
unsigned char analysis_end[8]; /* 50 */
} __attribute__ ((gcc_struct, __packed__));
+/*@
+ @ requires \valid_read(string + (0 .. max_length-1));
+ @ assigns \nothing;
+ @*/
static uint64_t ascii2int(const unsigned char *string, const unsigned int max_length)
{
uint64_t res=0;
unsigned int i;
+ /*@
+ @ loop invariant res <= 0x1999999999999998;
+ @ loop assigns res,i;
+ @*/
for(i=0;i<max_length;i++)
{
if(string[i]>='0' && string[i]<='9')
+ {
res=res*10+(string[i]-'0');
+ if(res > 0x1999999999999998)
+ return 0xffffffffffffffff;
+ }
else if(!(string[i]==' ' && res==0))
return 0;
}
return res;
}
+/*@
+ @ requires \valid_read(string + (0 .. max_length-1));
+ @ assigns \nothing;
+ @*/
static uint64_t ascii2int2(const unsigned char *string, const unsigned int max_length, const unsigned int delimiter)
{
uint64_t res=0;
unsigned int i;
+ /*@
+ @ loop invariant res <= 0x1999999999999998;
+ @ loop assigns res,i;
+ @*/
for(i=0;i<max_length;i++)
+ {
if(string[i]>='0' && string[i]<='9')
+ {
res=res*10+(string[i]-'0');
+ if(res > 0x1999999999999998)
+ return res;
+ }
else if(string[i]==delimiter)
return res;
else if(string[i]==' ' && res>0)
return res;
else if(string[i]!=' ')
return 0;
+ }
return res;
}
+/*@
+ @ 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 fcs_header);
+ @ requires separation: \separated(&file_hint_fcs, 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->min_filesize == 58);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size > 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_fcs.extension);
+ @ 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);
+ @*/
static int header_check_fcs(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 fcs_header *fcs=(const struct fcs_header*)buffer;
@@ -114,8 +168,11 @@ static int header_check_fcs(const unsigned char *buffer, const unsigned int buff
if((data_end==0 || analysis_end==0) && text_start < buffer_size)
{ /* Explore TEXT segment */
unsigned int i;
- const char delimiter=buffer[text_start];
+ const unsigned char delimiter=buffer[text_start];
const unsigned int smallest=(buffer_size < text_end ? buffer_size : text_end);
+ /*@
+ @ loop assigns i, data_end, stext_end, analysis_end;
+ @*/
for(i=0; i<smallest; i++)
{
if(buffer[i]==delimiter)
@@ -137,6 +194,10 @@ static int header_check_fcs(const unsigned char *buffer, const unsigned int buff
log_info("$ENDSTEXT %llu\n", (long long unsigned) stext_end);
log_info("$ENDANALYSIS %llu\n", (long long unsigned) analysis_end);
#endif
+ if( data_end >= 0x8000000000000000 - 9 ||
+ analysis_end >= 0x8000000000000000 - 9 ||
+ stext_end >= 0x8000000000000000 - 9)
+ return 0;
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_fcs.extension;
file_recovery_new->min_filesize=58;
@@ -149,4 +210,10 @@ static int header_check_fcs(const unsigned char *buffer, const unsigned int buff
file_recovery_new->file_check=&file_check_size;
return 1;
}
+
+static void register_header_check_fcs(file_stat_t *file_stat)
+{
+ static const unsigned char fcs_signature[6]= {'F','C','S','3','.','0'};
+ register_header_check(0, fcs_signature, sizeof(fcs_signature), &header_check_fcs, file_stat);
+}
#endif