diff options
| author | Christophe Grenier <[email protected]> | 2023-10-08 14:31:56 +0200 |
|---|---|---|
| committer | Christophe Grenier <[email protected]> | 2023-10-08 14:31:56 +0200 |
| commit | 7c660ff10b0c903065143e0322f7737ba0f47a9f (patch) | |
| tree | 1a6237e00e9c28dfddb4bc36786345d0d8205748 /src/file_tib.c | |
| parent | 1941a27e94a1da627d9f574c03797f131478aadf (diff) | |
src/file*.c: add various Frama-C annotations in data_check_*()
Diffstat (limited to 'src/file_tib.c')
| -rw-r--r-- | src/file_tib.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/file_tib.c b/src/file_tib.c index c044ce38..53b1099f 100644 --- a/src/file_tib.c +++ b/src/file_tib.c @@ -57,6 +57,8 @@ static const unsigned char tib2_footer[7]= {0x00, 0x00, 0x20, 0xa2, 0xb9, 0x24, @*/ static data_check_t data_check_tib2(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) { + /*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */ + /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */ /*@ loop assigns file_recovery->calculated_file_size; */ while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size && file_recovery->calculated_file_size + 512 <= file_recovery->file_size + buffer_size/2) |