diff options
| author | Christophe Grenier <grenier@cgsecurity.org> | 2023-12-27 10:48:29 +0100 |
|---|---|---|
| committer | Christophe Grenier <grenier@cgsecurity.org> | 2023-12-27 10:48:29 +0100 |
| commit | 7002eed1605df7ade60eec4c4ebb5bfbeec84c31 (patch) | |
| tree | 617d76b804fd5537e0d6791d1d993341108fb486 | |
| parent | 81fb8018e62d03bda4029fd028f85bdde9acbf4b (diff) | |
src/file_axx.c: more frama-c annotations
| -rw-r--r-- | src/file_axx.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/file_axx.c b/src/file_axx.c index c625fd35..191c9512 100644 --- a/src/file_axx.c +++ b/src/file_axx.c @@ -64,6 +64,7 @@ static void file_check_axx(file_recovery_t *fr) /*@ @ loop assigns *fr->handle, errno, fr->file_size; @ loop assigns offset, Frama_C_entropy_source; + @ loop variant 0x8000000000000000 - offset; @ */ while(offset < 0x8000000000000000) { @@ -113,6 +114,7 @@ static void file_check_axx(file_recovery_t *fr) @ requires buffer_size > 0x25+sizeof(struct SHeader); @ requires separation: \separated(&file_hint_axx, 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); @ assigns *file_recovery_new; @*/ |