diff options
Diffstat (limited to 'src/file_rar.c')
| -rw-r--r-- | src/file_rar.c | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/src/file_rar.c b/src/file_rar.c index 9f0dd493..4291eff9 100644 --- a/src/file_rar.c +++ b/src/file_rar.c @@ -32,6 +32,7 @@ #include "filegen.h" +/*@ requires \valid(file_stat); */ static void register_header_check_rar(file_stat_t *file_stat); const file_hint_t file_hint_rar= { @@ -45,12 +46,31 @@ const file_hint_t file_hint_rar= { #define MHD_PASSWORD 0x0080U +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source); + @ requires file_recovery->file_check == &file_check_rar15fmt; + @ ensures \valid(file_recovery->handle); + @ assigns *file_recovery->handle, errno, file_recovery->file_size; + @ assigns Frama_C_entropy_source; + @*/ static void file_check_rar15fmt(file_recovery_t *file_recovery) { static const unsigned char rar15fmt_footer[7]={0xc4, 0x3d, 0x7b, 0x00, 0x40, 0x07, 0x00 }; file_search_footer(file_recovery, rar15fmt_footer, sizeof(rar15fmt_footer), 0); } +/*@ + @ requires buffer_size >= 0xb; + @ 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_rar, 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_rar15fmt(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) { reset_file_recovery(file_recovery_new); @@ -61,12 +81,31 @@ static int header_check_rar15fmt(const unsigned char *buffer, const unsigned int return 1; } +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source); + @ requires file_recovery->file_check == &file_check_rar50fmt; + @ ensures \valid(file_recovery->handle); + @ assigns *file_recovery->handle, errno, file_recovery->file_size; + @ assigns Frama_C_entropy_source; + @*/ static void file_check_rar50fmt(file_recovery_t *file_recovery) { static const unsigned char rar50fmt_footer[8]={0x1d, 0x77, 0x56, 0x51, 0x03, 0x05, 0x04, 0x00 }; file_search_footer(file_recovery, rar50fmt_footer, sizeof(rar50fmt_footer), 0); } +/*@ + @ requires buffer_size >= 0xb; + @ 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_rar, 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_rar50fmt(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) { reset_file_recovery(file_recovery_new); |