diff options
| author | Christophe Grenier <grenier@cgsecurity.org> | 2023-12-27 11:09:52 +0100 |
|---|---|---|
| committer | Christophe Grenier <grenier@cgsecurity.org> | 2023-12-27 11:09:52 +0100 |
| commit | 1f45f8193db0955e90145239dc80d81b14be8176 (patch) | |
| tree | bff34d1934c57f99f8c76d69291f4f8bf007b98a | |
| parent | 73a4d15048421076e6b131b5537d84ca632c254f (diff) | |
src/file_gsm.c: add more frama-c annotations
| -rw-r--r-- | src/file_gsm.c | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/file_gsm.c b/src/file_gsm.c index 4bef9de7..2c6ec284 100644 --- a/src/file_gsm.c +++ b/src/file_gsm.c @@ -54,6 +54,7 @@ struct block_header /*@ @ requires file_recovery->data_check==&data_check_gsm; @ requires valid_data_check_param(buffer, buffer_size, file_recovery); + @ terminates \true; @ ensures valid_data_check_result(\result, file_recovery); @ assigns file_recovery->calculated_file_size; @*/ @@ -63,6 +64,7 @@ static data_check_t data_check_gsm(const unsigned char *buffer, const unsigned i /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */ /*@ @ loop assigns file_recovery->calculated_file_size; + @ loop variant file_recovery->file_size + buffer_size/2 - (file_recovery->calculated_file_size + sizeof(struct block_header)); @*/ while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size && file_recovery->calculated_file_size + sizeof(struct block_header) < file_recovery->file_size + buffer_size/2) @@ -80,13 +82,17 @@ static data_check_t data_check_gsm(const unsigned char *buffer, const unsigned i /*@ @ requires separation: \separated(&file_hint_gsm, buffer+(..), file_recovery, file_recovery_new); @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); + @ terminates \true; @ ensures valid_header_check_result(\result, file_recovery_new); @*/ static int header_check_gsm(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) { unsigned int i=0; /*@ assert file_recovery_new->blocksize <= buffer_size; */ - /*@ loop assigns i; */ + /*@ + @ loop assigns i; + @ loop variant file_recovery_new->blocksize - (i+1) * sizeof(struct block_header); + @*/ for(i=0; (i+1) * sizeof(struct block_header) <= file_recovery_new->blocksize; i++) |