From cd787bb0974e801d3431e7574897f67da28a71dd Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sat, 10 Apr 2021 11:04:41 +0200 Subject: [PATCH] src/file_r3d.c: add Frama-C annotations --- src/file_r3d.c | 171 ++++++++++++++++++++++++++++++------------------- 1 file changed, 105 insertions(+), 66 deletions(-) diff --git a/src/file_r3d.c b/src/file_r3d.c index cfd0cebd..3d73e541 100644 --- a/src/file_r3d.c +++ b/src/file_r3d.c @@ -34,119 +34,158 @@ #include "common.h" #include "log.h" +/*@ requires \valid(file_stat); */ static void register_header_check_r3d(file_stat_t *file_stat); -static int header_check_r3d(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 void file_rename_r3d(file_recovery_t *file_recovery); -const file_hint_t file_hint_r3d= { - .extension="r3d", - .description="RED r3d camera", - .max_filesize=PHOTOREC_MAX_FILE_SIZE, - .recover=1, - .enable_by_default=1, - .register_header_check=®ister_header_check_r3d +const file_hint_t file_hint_r3d = { + .extension = "r3d", + .description = "RED r3d camera", + .max_filesize = PHOTOREC_MAX_FILE_SIZE, + .recover = 1, + .enable_by_default = 1, + .register_header_check = ®ister_header_check_r3d }; -static const unsigned char r3d_header1[4]= { 'R' , 'E' , 'D' , '1' }; -static const unsigned char r3d_header2[4]= { 'R' , 'E' , 'D' , '2' }; - struct atom_struct { uint32_t size; uint32_t type; -} __attribute__ ((gcc_struct, __packed__)); +} __attribute__((gcc_struct, __packed__)); +/*@ + @ 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_r3d; + @ requires \separated(buffer + (..), file_recovery); + @ ensures \result == DC_CONTINUE || \result == DC_STOP; + @ assigns file_recovery->calculated_file_size, file_recovery->data_check; + @*/ static data_check_t data_check_r3d(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) { - 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) + /*@ + @ loop assigns file_recovery->calculated_file_size; + @*/ + 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 struct atom_struct *atom=(const struct atom_struct*)&buffer[i]; - uint64_t atom_size=be32(atom->size); - if(atom_size<8) + const unsigned int i = file_recovery->calculated_file_size + buffer_size / 2 - file_recovery->file_size; + /*@ assert 0 <= i <= buffer_size-8; */ + const struct atom_struct *atom = (const struct atom_struct *)&buffer[i]; + uint64_t atom_size = be32(atom->size); + if(atom_size < 8) return DC_STOP; #ifdef DEBUG_R3D log_trace("file_r3d.c: %s atom %c%c%c%c (0x%02x%02x%02x%02x) size %llu, calculated_file_size %llu\n", - file_recovery->filename, - buffer[i+4],buffer[i+5],buffer[i+6],buffer[i+7], - buffer[i+4],buffer[i+5],buffer[i+6],buffer[i+7], - (long long unsigned)atom_size, - (long long unsigned)file_recovery->calculated_file_size); + file_recovery->filename, + buffer[i + 4], buffer[i + 5], buffer[i + 6], buffer[i + 7], + buffer[i + 4], buffer[i + 5], buffer[i + 6], buffer[i + 7], + (long long unsigned)atom_size, + (long long unsigned)file_recovery->calculated_file_size); #endif - if(buffer[i+4]=='R' && buffer[i+5]=='E' && buffer[i+6]=='O') + if(buffer[i + 4] == 'R' && buffer[i + 5] == 'E' && buffer[i + 6] == 'O') { /* End of file */ - file_recovery->calculated_file_size+=atom_size; - file_recovery->data_check=NULL; + file_recovery->calculated_file_size += atom_size; + file_recovery->data_check = NULL; return DC_CONTINUE; } - if(buffer[i+4]!='R') + if(buffer[i + 4] != 'R') { return DC_STOP; } /* REDV1 REDV RPAD RDVO RDVS RDAO RDAS REOB */ - file_recovery->calculated_file_size+=atom_size; + file_recovery->calculated_file_size += atom_size; } #ifdef DEBUG_R3D log_trace("file_r3d.c: new calculated_file_size %llu\n", - (long long unsigned)file_recovery->calculated_file_size); + (long long unsigned)file_recovery->calculated_file_size); #endif return DC_CONTINUE; } -static int header_check_r3d(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) -{ - const struct atom_struct *atom=(const struct atom_struct*)buffer; - if(be32(atom->size) < 8) - return 0; - if(buffer[0xa]=='R' && buffer[0xb]=='1') - { - reset_file_recovery(file_recovery_new); - file_recovery_new->extension=file_hint_r3d.extension; - file_recovery_new->file_rename=&file_rename_r3d; - if(file_recovery_new->blocksize < 8) - return 1; - file_recovery_new->data_check=&data_check_r3d; - file_recovery_new->file_check=&file_check_size; - return 1; - } - return 0; -} - -static int header_check_r3d_v2(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[0xa]=='R' && buffer[0xb]=='2') - { - reset_file_recovery(file_recovery_new); - file_recovery_new->extension=file_hint_r3d.extension; - return 1; - } - return 0; -} - +/*@ + @ requires \valid(file_recovery); + @ requires valid_file_recovery(file_recovery); + @ requires file_recovery->file_rename==&file_rename_r3d; + @*/ static void file_rename_r3d(file_recovery_t *file_recovery) { unsigned char buffer[512]; FILE *file; size_t buffer_size; unsigned int i; - if((file=fopen(file_recovery->filename, "rb"))==NULL) + if((file = fopen(file_recovery->filename, "rb")) == NULL) return; - buffer_size=fread(buffer, 1, sizeof(buffer), file); + buffer_size = fread(buffer, 1, sizeof(buffer), file); fclose(file); - if(buffer_size<0x44) + if(buffer_size < 0x44) return; - for(i=0x43; i< buffer_size && buffer[i]!=0 && buffer[i]!='.'; i++) + /*@ loop assigns i; */ + for(i = 0x43; i < buffer_size && buffer[i] != 0 && buffer[i] != '.'; i++) { - if(!isalnum(buffer[i]) && buffer[i]!='_') - return ; + if(!isalnum(buffer[i]) && buffer[i] != '_') + return; } file_rename(file_recovery, buffer, i, 0x43, NULL, 1); } +/*@ + @ requires buffer_size >= sizeof(struct atom_struct); + @ 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_r3d, buffer+(..), file_recovery, file_recovery_new); + @ ensures \result == 0 || \result == 1; + @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @ assigns *file_recovery_new; + @*/ +static int header_check_r3d(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) +{ + const struct atom_struct *atom = (const struct atom_struct *)buffer; + if(be32(atom->size) < 8) + return 0; + if(buffer[0xa] == 'R' && buffer[0xb] == '1') + { + reset_file_recovery(file_recovery_new); + file_recovery_new->extension = file_hint_r3d.extension; + file_recovery_new->file_rename = &file_rename_r3d; + if(file_recovery_new->blocksize < 8) + return 1; + file_recovery_new->data_check = &data_check_r3d; + file_recovery_new->file_check = &file_check_size; + return 1; + } + return 0; +} + +/*@ + @ requires buffer_size >= 0xc; + @ 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_r3d, buffer+(..), file_recovery, file_recovery_new); + @ ensures \result == 0 || \result == 1; + @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @ assigns *file_recovery_new; + @*/ +static int header_check_r3d_v2(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[0xa] == 'R' && buffer[0xb] == '2') + { + reset_file_recovery(file_recovery_new); + file_recovery_new->extension = file_hint_r3d.extension; + return 1; + } + return 0; +} + static void register_header_check_r3d(file_stat_t *file_stat) { + static const unsigned char r3d_header1[4] = { 'R', 'E', 'D', '1' }; + static const unsigned char r3d_header2[4] = { 'R', 'E', 'D', '2' }; register_header_check(4, r3d_header1, sizeof(r3d_header1), &header_check_r3d, file_stat); register_header_check(4, r3d_header2, sizeof(r3d_header2), &header_check_r3d_v2, file_stat); }