diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/file_mov.c | 1 | ||||
| -rw-r--r-- | src/file_zip.c | 14 | ||||
| -rw-r--r-- | src/filegen.h | 3 |
3 files changed, 17 insertions, 1 deletions
diff --git a/src/file_mov.c b/src/file_mov.c index 2246cd7..b330395 100644 --- a/src/file_mov.c +++ b/src/file_mov.c @@ -103,6 +103,7 @@ static void file_rename_mov(file_recovery_t *file_recovery) /*@ @ requires buffer_size >= 16; + @ requires (buffer_size&1)==0; @ requires \valid_read(buffer+(0..buffer_size-1)); @ requires \valid(file_recovery); @ requires file_recovery->data_check==&data_check_mov; diff --git a/src/file_zip.c b/src/file_zip.c index 50578d9..c674b2f 100644 --- a/src/file_zip.c +++ b/src/file_zip.c @@ -852,22 +852,29 @@ static void file_check_zip(file_recovery_t *fr) @ requires valid_read_string((char*)file_recovery->filename); @ requires file_recovery->file_rename==&file_rename_zip; @*/ +/* TODO ensures valid_read_string((char*)file_recovery->filename); */ static void file_rename_zip(file_recovery_t *file_recovery) { const char *ext=NULL; unsigned int file_nbr=0; file_recovery_t fr; reset_file_recovery(&fr); + /*@ assert valid_read_string((char*)file_recovery->filename); */ if((fr.handle=fopen(file_recovery->filename, "rb"))==NULL) + { + /*@ assert valid_read_string((char*)file_recovery->filename); */ return; + } fr.file_size = 0; fr.offset_error=0; first_filename[0]='\0'; if(my_fseek(fr.handle, 0, SEEK_SET) < 0) { fclose(fr.handle); + /*@ assert valid_read_string((char*)file_recovery->filename); */ return ; } + /*@ loop invariant valid_read_string((char*)file_recovery->filename); */ while (1) { uint32_t header; @@ -875,6 +882,7 @@ static void file_rename_zip(file_recovery_t *file_recovery) if(file_nbr>=0xffffffff || fr.file_size >= 0x8000000000000000 - 4) { fclose(fr.handle); + /*@ assert valid_read_string((char*)file_recovery->filename); */ return; } /*@ assert fr.file_size < 0x8000000000000000 - 4; */ @@ -885,6 +893,7 @@ static void file_rename_zip(file_recovery_t *file_recovery) log_trace("Failed to read block header\n"); #endif fclose(fr.handle); + /*@ assert valid_read_string((char*)file_recovery->filename); */ return; } #if defined(__FRAMAC__) @@ -921,7 +930,9 @@ static void file_rename_zip(file_recovery_t *file_recovery) if(ext!=NULL) { fclose(fr.handle); + /*@ assert valid_read_string((char*)file_recovery->filename); */ file_rename(file_recovery, NULL, 0, 0, ext, 1); + /*@ assert valid_read_string((char*)file_recovery->filename); */ return; } break; @@ -943,6 +954,7 @@ static void file_rename_zip(file_recovery_t *file_recovery) if (status<0) { fclose(fr.handle); + /*@ assert valid_read_string((char*)file_recovery->filename); */ return; } /* Only end of central dir is end of archive, 64b version of it is before */ @@ -956,7 +968,9 @@ static void file_rename_zip(file_recovery_t *file_recovery) first_filename[len]!='/' && first_filename[len]!='\\'; len++); + /*@ assert valid_read_string((char*)file_recovery->filename); */ file_rename(file_recovery, first_filename, len, 0, "zip", 0); + /*@ assert valid_read_string((char*)file_recovery->filename); */ return; } } diff --git a/src/filegen.h b/src/filegen.h index 7a1807b..a7ebde4 100644 --- a/src/filegen.h +++ b/src/filegen.h @@ -144,7 +144,8 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length); /*@ - @ requires buffer_size > 0; + @ requires buffer_size >= 2; + @ requires (buffer_size&1)==0; @ requires \valid_read((char *)buffer+(0..buffer_size-1)); @ requires \valid(file_recovery); @ requires file_recovery->data_check == &data_check_size; |