From 5d914f2a450a17e4de74757d2a27d2ed16a4c026 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Fri, 29 Jan 2021 19:09:18 +0100 Subject: [PATCH] src/file_dv.c: fix frama-c annotations for data_check_*() --- src/file_dv.c | 56 +++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 54 insertions(+), 2 deletions(-) diff --git a/src/file_dv.c b/src/file_dv.c index bc45ce37..39ff43a4 100644 --- a/src/file_dv.c +++ b/src/file_dv.c @@ -34,6 +34,7 @@ #include "__fc_builtin.h" #endif +/*@ requires \valid(file_stat); */ static void register_header_check_dv(file_stat_t *file_stat); const file_hint_t file_hint_dv= { @@ -45,6 +46,17 @@ const file_hint_t file_hint_dv= { .register_header_check=®ister_header_check_dv }; +/*@ + @ requires buffer_size > 0; + @ requires (buffer_size&1)==0; + @ requires \valid_read(buffer+(0..buffer_size-1)); + @ requires \valid(file_recovery); + @ requires file_recovery->data_check==&data_check_NTSC; + @ requires file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; + @ requires \separated(buffer, file_recovery); + @ ensures \result == DC_CONTINUE || \result == DC_STOP; + @ assigns file_recovery->calculated_file_size; + @*/ static data_check_t data_check_NTSC(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) { /*@ @@ -53,7 +65,8 @@ static data_check_t data_check_NTSC(const unsigned char *buffer, const unsigned while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size && file_recovery->calculated_file_size + 8 < file_recovery->file_size + buffer_size/2) { - const unsigned int i=file_recovery->calculated_file_size - file_recovery->file_size + buffer_size/2; + const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size; + /*@ assert 0 <= i < buffer_size - 8; */ if(buffer[i]==0x1f && buffer[i+1]==0x07 && buffer[i+2]==0x00 && buffer[i+5]==0x78 && buffer[i+6]==0x78 && buffer[i+7]==0x78) file_recovery->calculated_file_size+=120000; @@ -63,6 +76,13 @@ static data_check_t data_check_NTSC(const unsigned char *buffer, const unsigned return DC_CONTINUE; } +/*@ + @ requires \valid(fr); + @ requires fr->file_check == &file_check_dv_NTSC; + @ requires valid_file_recovery(fr); + @ ensures valid_file_recovery(fr); + @ assigns *fr->handle, errno, Frama_C_entropy_source, fr->file_size; + @*/ static void file_check_dv_NTSC(file_recovery_t *fr) { unsigned char buffer_header[512]; @@ -78,6 +98,7 @@ static void file_check_dv_NTSC(file_recovery_t *fr) fs-=120000; if(fs > 0) fs-=120000; + /*@ loop assigns fs, *fr->handle, errno, Frama_C_entropy_source, fr->file_size; */ while(fs < fr->file_size && my_fseek(fr->handle, fs, SEEK_SET) >= 0 && fread(&buffer, sizeof(buffer), 1, fr->handle) == 1) @@ -86,6 +107,7 @@ static void file_check_dv_NTSC(file_recovery_t *fr) #if defined(__FRAMAC__) Frama_C_make_unknown((char *)&buffer, sizeof(buffer)); #endif + /*@ loop assigns i, fr->file_size; */ for(i=1; ifile_size=fs; } +/*@ + @ requires buffer_size > 0; + @ requires (buffer_size&1)==0; + @ requires \valid_read(buffer+(0..buffer_size-1)); + @ requires \valid(file_recovery); + @ requires file_recovery->data_check==&data_check_PAL; + @ requires file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; + @ requires \separated(buffer, file_recovery); + @ ensures \result == DC_CONTINUE || \result == DC_STOP; + @ assigns file_recovery->calculated_file_size; + @*/ static data_check_t data_check_PAL(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) { /*@ @@ -105,7 +138,8 @@ static data_check_t data_check_PAL(const unsigned char *buffer, const unsigned i while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size && file_recovery->calculated_file_size + 8 < file_recovery->file_size + buffer_size/2) { - const unsigned int i=file_recovery->calculated_file_size - file_recovery->file_size + buffer_size/2; + const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size; + /*@ assert 0 <= i < buffer_size - 8; */ if(buffer[i]==0x1f && buffer[i+1]==0x07 && buffer[i+2]==0x00 && buffer[i+5]==0x78 && buffer[i+6]==0x78 && buffer[i+7]==0x78) file_recovery->calculated_file_size+=144000; @@ -115,6 +149,13 @@ static data_check_t data_check_PAL(const unsigned char *buffer, const unsigned i return DC_CONTINUE; } +/*@ + @ requires \valid(fr); + @ requires fr->file_check == &file_check_dv_PAL; + @ requires valid_file_recovery(fr); + @ ensures valid_file_recovery(fr); + @ assigns *fr->handle, errno, Frama_C_entropy_source, fr->file_size; + @*/ static void file_check_dv_PAL(file_recovery_t *fr) { unsigned char buffer_header[512]; @@ -130,6 +171,7 @@ static void file_check_dv_PAL(file_recovery_t *fr) fs-=144000; if(fs > 0) fs-=144000; + /*@ loop assigns fs, *fr->handle, errno, Frama_C_entropy_source, fr->file_size; */ while(fs < fr->file_size && my_fseek(fr->handle, fs, SEEK_SET) >= 0 && fread(&buffer, sizeof(buffer), 1, fr->handle) == 1) @@ -138,6 +180,7 @@ static void file_check_dv_PAL(file_recovery_t *fr) #if defined(__FRAMAC__) Frama_C_make_unknown((char *)&buffer, sizeof(buffer)); #endif + /*@ loop assigns i, fr->file_size; */ for(i=1; i= 8; + @ 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_dv, buffer+(..), file_recovery, file_recovery_new); + @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @*/ static int header_check_dv(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) { if(buffer[0]!=0x1f || buffer[1]!=0x07 || buffer[2]!=0x00 || buffer[5]!=0x78 || buffer[6]!=0x78 || buffer[7]!=0x78)