src/file_mig.c: fix Frama-C warnings

This commit is contained in:
Christophe Grenier 2021-07-02 18:48:54 +02:00
parent 02a92c5bb3
commit 23e422615d

View file

@ -35,7 +35,7 @@
#include "log.h" #include "log.h"
#endif #endif
/*@ requires \valid(file_stat); */ /*@ requires valid_register_header_check(file_stat); */
static void register_header_check_mig(file_stat_t *file_stat); static void register_header_check_mig(file_stat_t *file_stat);
const file_hint_t file_hint_mig= { const file_hint_t file_hint_mig= {
@ -61,16 +61,12 @@ struct MIG_HDR
} __attribute__ ((gcc_struct, __packed__)); } __attribute__ ((gcc_struct, __packed__));
/*@ /*@
@ requires valid_file_recovery(file_recovery);
@ requires \valid(file_recovery->handle);
@ 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_mig; @ requires file_recovery->file_check == &file_check_mig;
@ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
@ requires valid_file_check_param(file_recovery);
@ ensures valid_file_check_result(file_recovery);
@ assigns *file_recovery->handle, errno, file_recovery->file_size; @ assigns *file_recovery->handle, errno, file_recovery->file_size;
@ assigns Frama_C_entropy_source; @ assigns Frama_C_entropy_source;
@
@ ensures \valid(file_recovery->handle);
@*/ @*/
static void file_check_mig(file_recovery_t *file_recovery) static void file_check_mig(file_recovery_t *file_recovery)
{ {
@ -83,7 +79,8 @@ static void file_check_mig(file_recovery_t *file_recovery)
@*/ @*/
while(1) while(1)
{ {
struct MIG_HDR h; char buffer[sizeof(struct MIG_HDR)];
const struct MIG_HDR *h=(const struct MIG_HDR *)&buffer;
size_t res; size_t res;
if(my_fseek(file_recovery->handle, offset, SEEK_SET) < 0) if(my_fseek(file_recovery->handle, offset, SEEK_SET) < 0)
{ {
@ -92,7 +89,7 @@ static void file_check_mig(file_recovery_t *file_recovery)
#endif #endif
return ; return ;
} }
res=fread(&h, 1, sizeof(h), file_recovery->handle); res=fread(&buffer, 1, sizeof(buffer), file_recovery->handle);
if(res < 8) if(res < 8)
{ {
#ifdef DEBUG_MIG #ifdef DEBUG_MIG
@ -100,31 +97,28 @@ static void file_check_mig(file_recovery_t *file_recovery)
#endif #endif
return ; return ;
} }
if(res < sizeof(h) || le32(h.magic)!=0x5354524d) /* STRM=stream */ /* STRM=stream */
if(res < sizeof(buffer) || le32(h->magic)!=0x5354524d || offset >= PHOTOREC_MAX_FILE_SIZE)
{ {
#ifdef DEBUG_MIG #ifdef DEBUG_MIG
log_info("0x%lx no magic %x\n", (long unsigned)offset, le32(h.magic)); log_info("0x%lx no magic %x\n", (long unsigned)offset, le32(h->magic));
#endif #endif
file_recovery->file_size=offset+8; file_recovery->file_size=offset+8;
return ; return ;
} }
#ifdef DEBUG_MIG #ifdef DEBUG_MIG
log_info("0x%lx magic s_size=0x%u\n", (long unsigned)offset, le32(h.s_size)); log_info("0x%lx magic s_size=0x%u\n", (long unsigned)offset, le32(h->s_size));
#endif #endif
offset+=sizeof(h)+le32(h.s_size); offset+=sizeof(buffer)+le32(h->s_size);
} }
} }
/*@ /*@
@ requires buffer_size > 0x38; @ requires buffer_size > 0x38;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires valid_file_recovery(file_recovery);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(&file_hint_mig, buffer+(..), file_recovery, file_recovery_new); @ requires separation: \separated(&file_hint_mig, buffer+(..), file_recovery, file_recovery_new);
@ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
@ ensures valid_header_check_result(\result, file_recovery_new);
@ assigns *file_recovery_new; @ assigns *file_recovery_new;
@ ensures \result == 0 || \result == 1;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@*/ @*/
static int header_check_mig(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 int header_check_mig(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)
{ {