diff options
| author | Christophe Grenier <grenier@cgsecurity.org> | 2023-12-27 10:59:01 +0100 |
|---|---|---|
| committer | Christophe Grenier <grenier@cgsecurity.org> | 2023-12-27 10:59:01 +0100 |
| commit | bff55a22ba0d02603d82c92f02d4148d35ee07f5 (patch) | |
| tree | c8d3da71d4bb4afaefd9f2cf07cce7394a41a59d | |
| parent | 50d4181e76ec215c6b6d21c8c9563807e2325d65 (diff) | |
src/file_flv.c: more frama-c annotations
| -rw-r--r-- | src/file_flv.c | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/file_flv.c b/src/file_flv.c index 7299acab..16128833 100644 --- a/src/file_flv.c +++ b/src/file_flv.c @@ -110,6 +110,7 @@ static data_check_t data_check_flv(const unsigned char *buffer, const unsigned i @ requires buffer_size >= sizeof(struct flv_header); @ requires separation: \separated(&file_hint_flv, 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; @*/ |