From 2573eb40c36605b4ca8854ab1e83422a43b25856 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sun, 25 Jul 2021 10:58:01 +0200 Subject: [PATCH] src/file_tiff*.[ch]: Fix Frama-C warnings --- src/file_tiff.c | 2 +- src/file_tiff.h | 48 ++++++---------------------------------------- src/file_tiff_be.c | 21 ++++++++------------ src/file_tiff_le.c | 11 ++++++----- 4 files changed, 21 insertions(+), 61 deletions(-) diff --git a/src/file_tiff.c b/src/file_tiff.c index 17edb1f9..a5f00cfc 100644 --- a/src/file_tiff.c +++ b/src/file_tiff.c @@ -43,7 +43,7 @@ #include "__fc_builtin.h" #endif -/*@ requires \valid(file_stat); */ +/*@ requires valid_register_header_check(file_stat); */ static void register_header_check_tiff(file_stat_t *file_stat); const file_hint_t file_hint_tiff= { diff --git a/src/file_tiff.h b/src/file_tiff.h index d74e721f..12df8161 100644 --- a/src/file_tiff.h +++ b/src/file_tiff.h @@ -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) /*@ - @ 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 separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); - @ ensures \valid(fr->handle); - @ ensures valid_read_string(fr->extension); + @ requires valid_file_check_param(fr); + @ ensures valid_file_check_result(fr); @ assigns errno; @ assigns fr->file_size; @ 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) /*@ - @ 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; - @ - @ 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); + @ 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); @ 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) ==> 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->data_check == \null); @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_tiff_le); @ 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); #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) /*@ - @ 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; - @ - @ 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); + @ 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); @ 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) ==> 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->data_check == \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); #endif diff --git a/src/file_tiff_be.c b/src/file_tiff_be.c index b667b64a..3a3d9905 100644 --- a/src/file_tiff_be.c +++ b/src/file_tiff_be.c @@ -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 separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); - @ ensures \valid(fr->handle); - @ ensures valid_read_string(fr->extension); + @ requires valid_file_check_param(fr); + @ ensures valid_file_check_result(fr); @ assigns errno; @ assigns fr->file_size; @ 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 uint64_t calculated_file_size=0; - TIFFHeader header; + char buffer[sizeof(TIFFHeader)]; + const TIFFHeader *header=(const TIFFHeader *)&buffer; calculated_file_size = 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; return; } #if defined(__FRAMAC__) - Frama_C_make_unknown((char *)&header, sizeof(TIFFHeader)); + Frama_C_make_unknown(&buffer, sizeof(TIFFHeader)); #endif - if(header.tiff_magic==TIFF_BIGENDIAN) - calculated_file_size=file_check_tiff_be_aux(fr, be32(header.tiff_diroff), 0, 0); + if(header->tiff_magic==TIFF_BIGENDIAN) + calculated_file_size=file_check_tiff_be_aux(fr, be32(header->tiff_diroff), 0, 0); /*@ assert \valid(fr->handle); */ #ifdef DEBUG_TIFF log_info("TIFF Current %llu\n", (unsigned long long)fr->file_size); diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c index f12d98ee..f597d46d 100644 --- a/src/file_tiff_le.c +++ b/src/file_tiff_le.c @@ -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) { static uint64_t calculated_file_size=0; - TIFFHeader header; + char buffer[sizeof(TIFFHeader)]; + const TIFFHeader *header=(const TIFFHeader *)&buffer; calculated_file_size = 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; return; } #if defined(__FRAMAC__) - Frama_C_make_unknown((char *)&header, sizeof(TIFFHeader)); + Frama_C_make_unknown(&buffer, sizeof(TIFFHeader)); #endif - if(header.tiff_magic==TIFF_LITTLEENDIAN) - calculated_file_size=file_check_tiff_le_aux(fr, le32(header.tiff_diroff), 0, 0); + if(header->tiff_magic==TIFF_LITTLEENDIAN) + calculated_file_size=file_check_tiff_le_aux(fr, le32(header->tiff_diroff), 0, 0); /*@ assert \valid(fr->handle); */ #ifdef DEBUG_TIFF log_info("TIFF Current %llu\n", (unsigned long long)fr->file_size);