src/file_tiff*.[ch]: Fix Frama-C warnings

This commit is contained in:
Christophe Grenier 2021-07-25 10:58:01 +02:00
parent d8ca0f4608
commit 2573eb40c3
4 changed files with 21 additions and 61 deletions

View file

@ -43,7 +43,7 @@
#include "__fc_builtin.h" #include "__fc_builtin.h"
#endif #endif
/*@ requires \valid(file_stat); */ /*@ requires valid_register_header_check(file_stat); */
static void register_header_check_tiff(file_stat_t *file_stat); static void register_header_check_tiff(file_stat_t *file_stat);
const file_hint_t file_hint_tiff= { const file_hint_t file_hint_tiff= {

View file

@ -98,15 +98,9 @@ unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const uns
#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) #if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg)
/*@ /*@
@ requires \valid(fr);
@ requires \valid(fr->handle);
@ requires valid_file_recovery(fr);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
@ requires fr->file_check==&file_check_tiff_le; @ requires fr->file_check==&file_check_tiff_le;
@ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ requires valid_file_check_param(fr);
@ ensures \valid(fr->handle); @ ensures valid_file_check_result(fr);
@ ensures valid_read_string(fr->extension);
@ assigns errno; @ assigns errno;
@ assigns fr->file_size; @ assigns fr->file_size;
@ assigns *fr->handle; @ assigns *fr->handle;
@ -117,31 +111,16 @@ void file_check_tiff_le(file_recovery_t *fr);
#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf) && !defined(SINGLE_FORMAT_wdp) #if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf) && !defined(SINGLE_FORMAT_wdp)
/*@ /*@
@ 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 >= 15; @ requires buffer_size >= 15;
@ @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
@ ensures \result == 0 || \result == 1; @ ensures valid_header_check_result(\result, file_recovery_new);
@ 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) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> \initialized(&file_recovery_new->min_filesize);
@ ensures (\result == 1) ==> (file_recovery_new->extension != \null); @ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
@ 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);
@
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0); @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == \null); @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_tiff_le); @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_tiff_le);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null); @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@*/ @*/
int header_check_tiff_le(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); int header_check_tiff_le(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);
#endif #endif
@ -160,30 +139,15 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsi
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf) && !defined(SINGLE_FORMAT_wdp) #if !defined(MAIN_tiff_le) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf) && !defined(SINGLE_FORMAT_wdp)
/*@ /*@
@ 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 >= 15; @ requires buffer_size >= 15;
@ @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
@ ensures \result == 0 || \result == 1; @ ensures valid_header_check_result(\result, file_recovery_new);
@ 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) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> \initialized(&file_recovery_new->min_filesize);
@ ensures (\result == 1) ==> (file_recovery_new->extension != \null); @ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
@ 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);
@
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0); @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == \null); @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null); @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@*/ @*/
int header_check_tiff_be(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); int header_check_tiff_be(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);
#endif #endif

View file

@ -712,15 +712,9 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
} }
/*@ /*@
@ requires \valid(fr);
@ requires \valid(fr->handle);
@ requires valid_file_recovery(fr);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
@ requires fr->file_check==&file_check_tiff_be; @ requires fr->file_check==&file_check_tiff_be;
@ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ requires valid_file_check_param(fr);
@ ensures \valid(fr->handle); @ ensures valid_file_check_result(fr);
@ ensures valid_read_string(fr->extension);
@ assigns errno; @ assigns errno;
@ assigns fr->file_size; @ assigns fr->file_size;
@ assigns *fr->handle; @ assigns *fr->handle;
@ -729,19 +723,20 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
static void file_check_tiff_be(file_recovery_t *fr) static void file_check_tiff_be(file_recovery_t *fr)
{ {
static uint64_t calculated_file_size=0; static uint64_t calculated_file_size=0;
TIFFHeader header; char buffer[sizeof(TIFFHeader)];
const TIFFHeader *header=(const TIFFHeader *)&buffer;
calculated_file_size = 0; calculated_file_size = 0;
if(fseek(fr->handle, 0, SEEK_SET) < 0 || if(fseek(fr->handle, 0, SEEK_SET) < 0 ||
fread(&header, sizeof(TIFFHeader), 1, fr->handle) != 1) fread(&buffer, sizeof(TIFFHeader), 1, fr->handle) != 1)
{ {
fr->file_size=0; fr->file_size=0;
return; return;
} }
#if defined(__FRAMAC__) #if defined(__FRAMAC__)
Frama_C_make_unknown((char *)&header, sizeof(TIFFHeader)); Frama_C_make_unknown(&buffer, sizeof(TIFFHeader));
#endif #endif
if(header.tiff_magic==TIFF_BIGENDIAN) if(header->tiff_magic==TIFF_BIGENDIAN)
calculated_file_size=file_check_tiff_be_aux(fr, be32(header.tiff_diroff), 0, 0); calculated_file_size=file_check_tiff_be_aux(fr, be32(header->tiff_diroff), 0, 0);
/*@ assert \valid(fr->handle); */ /*@ assert \valid(fr->handle); */
#ifdef DEBUG_TIFF #ifdef DEBUG_TIFF
log_info("TIFF Current %llu\n", (unsigned long long)fr->file_size); log_info("TIFF Current %llu\n", (unsigned long long)fr->file_size);

View file

@ -726,19 +726,20 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
void file_check_tiff_le(file_recovery_t *fr) void file_check_tiff_le(file_recovery_t *fr)
{ {
static uint64_t calculated_file_size=0; static uint64_t calculated_file_size=0;
TIFFHeader header; char buffer[sizeof(TIFFHeader)];
const TIFFHeader *header=(const TIFFHeader *)&buffer;
calculated_file_size = 0; calculated_file_size = 0;
if(fseek(fr->handle, 0, SEEK_SET) < 0 || if(fseek(fr->handle, 0, SEEK_SET) < 0 ||
fread(&header, sizeof(TIFFHeader), 1, fr->handle) != 1) fread(&buffer, sizeof(TIFFHeader), 1, fr->handle) != 1)
{ {
fr->file_size=0; fr->file_size=0;
return; return;
} }
#if defined(__FRAMAC__) #if defined(__FRAMAC__)
Frama_C_make_unknown((char *)&header, sizeof(TIFFHeader)); Frama_C_make_unknown(&buffer, sizeof(TIFFHeader));
#endif #endif
if(header.tiff_magic==TIFF_LITTLEENDIAN) if(header->tiff_magic==TIFF_LITTLEENDIAN)
calculated_file_size=file_check_tiff_le_aux(fr, le32(header.tiff_diroff), 0, 0); calculated_file_size=file_check_tiff_le_aux(fr, le32(header->tiff_diroff), 0, 0);
/*@ assert \valid(fr->handle); */ /*@ assert \valid(fr->handle); */
#ifdef DEBUG_TIFF #ifdef DEBUG_TIFF
log_info("TIFF Current %llu\n", (unsigned long long)fr->file_size); log_info("TIFF Current %llu\n", (unsigned long long)fr->file_size);