luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

src/file_dovecot.c: fix wrong Frama-C annotations for data_check_dovecot2()

Browse source
This commit is contained in:
Christophe Grenier 2023-10-08 14:30:38 +02:00
parent 251ac27971
commit 126b9fafe5
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/file_dovecot.c
View file

@ -52,9 +52,8 @@ const file_hint_t file_hint_dovecot= {
@*/ @*/
static data_check_t data_check_dovecot2(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) static data_check_t data_check_dovecot2(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{ {
/*@ /*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */
@ loop assigns file_recovery->data_check; /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
@*/
if(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size && if(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size &&
file_recovery->calculated_file_size + 2 <= file_recovery->file_size + buffer_size/2) file_recovery->calculated_file_size + 2 <= file_recovery->file_size + buffer_size/2)
{ {