diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/file_icc.c | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/file_icc.c b/src/file_icc.c index f5400918..72ebec80 100644 --- a/src/file_icc.c +++ b/src/file_icc.c @@ -30,6 +30,7 @@ #include "types.h" #include "filegen.h" +/*@ requires \valid(file_stat); */ static void register_header_check_icc(file_stat_t *file_stat); const file_hint_t file_hint_icc= { @@ -41,6 +42,17 @@ const file_hint_t file_hint_icc= { .register_header_check=®ister_header_check_icc }; +/*@ + @ requires buffer_size >= 128; + @ 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_icc, 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_icc(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 uint64_t file_size=(((uint64_t)buffer[0])<<24) + @@ -48,6 +60,7 @@ static int header_check_icc(const unsigned char *buffer, const unsigned int buff unsigned int i; if(file_size<128 || buffer[10]!=0 || buffer[11]!=0) return 0; + /*@ loop assigns i; */ for(i=100; i<128; i++) if(buffer[i]!=0) return 0; |