diff options
| author | Christophe Grenier <grenier@cgsecurity.org> | 2024-05-18 16:06:50 +0200 |
|---|---|---|
| committer | Christophe Grenier <grenier@cgsecurity.org> | 2024-05-18 16:06:50 +0200 |
| commit | 037634c8d562cf20fcaaf88ce00679189fd47d36 (patch) | |
| tree | de440294d417432746f67f56c43a7cd981564e69 /src | |
| parent | 2c6780ca1edd0b0ba2e5e86b12634e3cc8475872 (diff) | |
src/file_jpg.c: jpg_search_marker() - add annotations so Frama-C knows
the function terminates
Diffstat (limited to 'src')
| -rw-r--r-- | src/file_jpg.c | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/file_jpg.c b/src/file_jpg.c index 99fbba42..6c0f48b8 100644 --- a/src/file_jpg.c +++ b/src/file_jpg.c @@ -1978,6 +1978,9 @@ static void jpg_search_marker(file_recovery_t *file_recovery) /*@ assert offset_test == offset_error; */ if(file_recovery->blocksize==0) return ; + if(offset_test > 0x80000000) + return ; + /*@ assert offset_test <= 0x80000000; */ offset=offset_test / file_recovery->blocksize * file_recovery->blocksize; if(my_fseek(infile, offset, SEEK_SET) < 0) return ; @@ -1989,6 +1992,7 @@ static void jpg_search_marker(file_recovery_t *file_recovery) @ loop assigns Frama_C_entropy_source; @ loop assigns offset, offset_test; @ loop assigns file_recovery->extra; + @ loop variant 0x80000000 + sizeof(sbuffer) - offset_test; @*/ while((nbytes=fread(&sbuffer, 1, sizeof(sbuffer), infile))>0) { |