diff options
| author | Christophe Grenier <grenier@cgsecurity.org> | 2023-12-27 11:13:55 +0100 |
|---|---|---|
| committer | Christophe Grenier <grenier@cgsecurity.org> | 2023-12-27 11:13:55 +0100 |
| commit | a7c9b753f4e92c026d55b8af8010ce54094d5b55 (patch) | |
| tree | 6d816b5b138a46fe6148acc4dee1fd9ab9c5d086 /src | |
| parent | 45900dbd73bf9339d603b45bb3d0d126cc2e8cab (diff) | |
src/file_ico.c: more frama-c annotations
Diffstat (limited to 'src')
| -rw-r--r-- | src/file_ico.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/file_ico.c b/src/file_ico.c index 6e9bc2c5..1a9becd1 100644 --- a/src/file_ico.c +++ b/src/file_ico.c @@ -82,6 +82,7 @@ struct ico_directory @ requires buffer_size >= sizeof(struct ico_header); @ requires separation: \separated(&file_hint_ico, 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; @*/ @@ -98,6 +99,7 @@ static int header_check_ico(const unsigned char *buffer, const unsigned int buff return 0; /*@ @ loop assigns ico_dir, i, fs; + @ loop variant le16(ico->count) - i; @*/ for(i=0, ico_dir=(const struct ico_directory*)(ico+1); (const unsigned char *)(ico_dir+1) <= buffer+buffer_size && i<le16(ico->count); |