From 50b90cd0dce477f08f3f633ba85fcda83e60a30e Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Tue, 9 Mar 2021 07:53:03 +0100 Subject: [PATCH] src/file_ttiff*.[ch]: improve Frama-C annotations --- src/file_tiff.h | 14 ++++++++------ src/file_tiff_be.c | 35 ++++++++++++++++++++++------------- src/file_tiff_le.c | 12 +++++------- 3 files changed, 35 insertions(+), 26 deletions(-) diff --git a/src/file_tiff.h b/src/file_tiff.h index 529303fc..3e7b0f96 100644 --- a/src/file_tiff.h +++ b/src/file_tiff.h @@ -100,11 +100,17 @@ unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const uns /*@ @ 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); + @ assigns errno; + @ assigns fr->file_size; + @ assigns *fr->handle; + @ assigns Frama_C_entropy_source; @*/ void file_check_tiff_le(file_recovery_t *fr); #endif @@ -127,9 +133,6 @@ void file_check_tiff_le(file_recovery_t *fr); @ 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 == 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); @@ -138,6 +141,7 @@ void file_check_tiff_le(file_recovery_t *fr); @ 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 @@ -172,9 +176,6 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsi @ 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 == 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); @@ -182,6 +183,7 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsi @ 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 48d811b2..51c9d8cd 100644 --- a/src/file_tiff_be.c +++ b/src/file_tiff_be.c @@ -244,6 +244,9 @@ static uint64_t parse_strip_be(FILE *handle, const TIFFDirEntry *entry_strip_off Frama_C_make_unknown((char *)offsetp, nbr*sizeof(*offsetp)); Frama_C_make_unknown((char *)sizep, nbr*sizeof(*sizep)); #endif + /*@ + @ loop assigns i, max_offset; + @*/ for(i=0; ihandle); + @ requires valid_file_recovery(fr); @ requires \valid_read(&fr->extension); @ requires valid_read_string(fr->extension); - @ requires \separated(&errno, fr); + @ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ requires \valid_read(buffer + (0 .. buffer_size - 1)); @ ensures \valid(fr); @ ensures \valid(fr->handle); @@ -425,9 +429,10 @@ static uint64_t file_check_tiff_be_aux_next(file_recovery_t *fr, const unsigned /*@ @ requires \valid(fr); @ requires \valid(fr->handle); + @ requires valid_file_recovery(fr); @ requires \valid_read(&fr->extension); @ requires valid_read_string(fr->extension); - @ requires \separated(&errno, fr); + @ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ ensures \valid(fr); @ ensures \valid(fr->handle); @ ensures valid_read_string(fr->extension); @@ -437,19 +442,19 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_ unsigned char buffer[8192]; unsigned int i,n; int data_read; - uint64_t max_offset=0; - uint64_t alphaoffset=0; uint64_t alphabytecount=0; - uint64_t imageoffset=0; + uint64_t alphaoffset=0; uint64_t imagebytecount=0; - uint64_t jpegifoffset=0; + uint64_t imageoffset=0; uint64_t jpegifbytecount=0; - uint64_t strip_offsets=0; + uint64_t jpegifoffset=0; + uint64_t max_offset=0; uint64_t strip_bytecounts=0; - uint64_t tile_offsets=0; + uint64_t strip_offsets=0; uint64_t tile_bytecounts=0; - unsigned int tdir_tag_old=0; + uint64_t tile_offsets=0; unsigned int sorted_tag_error=0; + unsigned int tdir_tag_old=0; const TIFFDirEntry *entries=(const TIFFDirEntry *)&buffer[2]; const TIFFDirEntry *entry_strip_offsets=NULL; const TIFFDirEntry *entry_strip_bytecounts=NULL; @@ -619,10 +624,6 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_ #if defined(__FRAMAC__) Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp)); #endif - /*X - X loop invariant 0 <= j <= nbr <=32; - X loop variant nbr-j; - X*/ for(j=0; jhandle); + @ 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); + @ assigns errno; + @ assigns fr->file_size; + @ assigns *fr->handle; + @ assigns Frama_C_entropy_source; @*/ static void file_check_tiff_be(file_recovery_t *fr) { diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c index 97898cbf..05a91a7e 100644 --- a/src/file_tiff_le.c +++ b/src/file_tiff_le.c @@ -395,9 +395,10 @@ static uint64_t file_check_tiff_le_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 \separated(&errno, fr); + @ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ requires \valid_read(buffer + (0 .. buffer_size - 1)); @ ensures \valid(fr); @ ensures \valid(fr->handle); @@ -432,9 +433,10 @@ static uint64_t file_check_tiff_le_aux_next(file_recovery_t *fr, const unsigned /*@ @ requires \valid(fr); @ requires \valid(fr->handle); + @ requires valid_file_recovery(fr); @ requires \valid_read(&fr->extension); @ requires valid_read_string(fr->extension); - @ requires \separated(&errno, fr); + @ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ ensures \valid(fr); @ ensures \valid(fr->handle); @ ensures valid_read_string(fr->extension); @@ -455,8 +457,8 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_ uint64_t strip_offsets=0; uint64_t tile_bytecounts=0; uint64_t tile_offsets=0; - unsigned int tdir_tag_old=0; unsigned int sorted_tag_error=0; + unsigned int tdir_tag_old=0; const TIFFDirEntry *entries=(const TIFFDirEntry *)&buffer[2]; const TIFFDirEntry *entry_strip_offsets=NULL; const TIFFDirEntry *entry_strip_bytecounts=NULL; @@ -634,10 +636,6 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_ #if defined(__FRAMAC__) Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp)); #endif - /*X - X loop invariant 0 <= j <= nbr <=32; - X loop variant nbr-j; - X*/ for(j=0; j