From b932ef701fbfb9e4a66406e076be67d4a2bebfaf Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sun, 6 Jun 2021 14:58:32 +0200 Subject: [PATCH] src/file_bmp.c: fix Frama-C annotations --- src/file_bmp.c | 37 ++++++++++++++++--------------------- src/filegen.c | 3 +++ src/filegen.h | 3 +++ 3 files changed, 22 insertions(+), 21 deletions(-) diff --git a/src/file_bmp.c b/src/file_bmp.c index 841ed92a..9d8b1df8 100644 --- a/src/file_bmp.c +++ b/src/file_bmp.c @@ -35,6 +35,9 @@ #include "__fc_builtin.h" #endif +/*@ + @ requires valid_register_header_check(file_stat); + @*/ static void register_header_check_bmp(file_stat_t *file_stat); const file_hint_t file_hint_bmp= { @@ -59,12 +62,19 @@ struct bmp_header /*@ @ requires buffer_size >= 18; - @ requires \valid_read(buffer+(0..buffer_size-1)); - @ requires \valid_read(file_recovery); - @ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename); - @ requires \valid(file_recovery_new); - @ requires file_recovery_new->blocksize > 0; @ requires separation: \separated(&file_hint_bmp, buffer+(..), file_recovery, file_recovery_new); + @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); + @ ensures valid_header_check_result(\result, file_recovery_new); + @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null); + @ ensures (\result == 1) ==> (file_recovery_new->handle == \null); + @ ensures (\result == 1) ==> (file_recovery_new->time == 0); + @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_bmp.extension); + @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 65); + @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0); + @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 65); + @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size); + @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size); + @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null); @ assigns file_recovery_new->filename[0]; @ assigns file_recovery_new->time; @ assigns file_recovery_new->file_stat; @@ -86,19 +96,7 @@ struct bmp_header @ assigns file_recovery_new->checkpoint_offset; @ assigns file_recovery_new->flags; @ assigns file_recovery_new->extra; - @ ensures \result == 0 || \result == 1; - @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null); - @ ensures (\result == 1) ==> (file_recovery_new->handle == \null); - @ ensures (\result == 1) ==> \initialized(&file_recovery_new->time); - @ ensures (\result == 1) ==> (file_recovery_new->time == 0); - @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_bmp.extension); - @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 65); - @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0); - @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 65); - @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size); - @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size); - @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null); - @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension)); + @ assigns file_recovery_new->data_check_tmp; @*/ // ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension); static int header_check_bmp(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) @@ -136,9 +134,6 @@ static int header_check_bmp(const unsigned char *buffer, const unsigned int buff return 0; } -/*@ - @ requires \valid(file_stat); - @*/ static void register_header_check_bmp(file_stat_t *file_stat) { register_header_check(0, bmp_header,sizeof(bmp_header), &header_check_bmp, file_stat); diff --git a/src/filegen.c b/src/filegen.c index 975751ee..aacac1c0 100644 --- a/src/filegen.c +++ b/src/filegen.c @@ -113,6 +113,8 @@ static void file_check_add_tail(file_check_t *file_check_new, file_check_list_t /*@ @ loop unroll 256; @ loop invariant 0 <= i <= 256; + @ loop invariant \forall integer j; (0 <= j < i) ==> newe->file_checks[j].list.prev == &newe->file_checks[j].list; + @ loop invariant \forall integer j; (0 <= j < i) ==> newe->file_checks[j].list.next == &newe->file_checks[j].list; @ loop assigns i, newe->file_checks[0 .. i-1].list.prev, newe->file_checks[0 .. i-1].list.next; @ loop variant 255-i; @*/ @@ -398,6 +400,7 @@ void reset_file_recovery(file_recovery_t *file_recovery) file_recovery->checkpoint_offset=0; file_recovery->flags=0; file_recovery->extra=0; + file_recovery->data_check_tmp=0; } file_stat_t * init_file_stats(file_enable_t *files_enable) diff --git a/src/filegen.h b/src/filegen.h index f20b60d3..6fe571aa 100644 --- a/src/filegen.h +++ b/src/filegen.h @@ -101,6 +101,7 @@ struct file_recovery_struct int checkpoint_status; /* 0=suspend at offset_checkpoint if offset_checkpoint>0, 1=resume at offset_checkpoint */ unsigned int blocksize; unsigned int flags; + unsigned int data_check_tmp; }; typedef struct @@ -300,6 +301,7 @@ void file_check_size_max(file_recovery_t *file_recovery); ensures file_recovery->checkpoint_offset==0; ensures file_recovery->flags==0; ensures file_recovery->extra==0; + ensures file_recovery->data_check_tmp==0; assigns file_recovery->filename[0]; assigns file_recovery->time; assigns file_recovery->file_stat; @@ -321,6 +323,7 @@ void file_check_size_max(file_recovery_t *file_recovery); assigns file_recovery->checkpoint_offset; assigns file_recovery->flags; assigns file_recovery->extra; + assigns file_recovery->data_check_tmp; */ // ensures valid_file_recovery(file_recovery); void reset_file_recovery(file_recovery_t *file_recovery);