From 126b9fafe534cc1b4785e67f3a56040c0ec4a40b Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sun, 8 Oct 2023 14:30:38 +0200 Subject: [PATCH] src/file_dovecot.c: fix wrong Frama-C annotations for data_check_dovecot2() --- src/file_dovecot.c | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/file_dovecot.c b/src/file_dovecot.c index c1f4c20c..70011b66 100644 --- a/src/file_dovecot.c +++ b/src/file_dovecot.c @@ -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) { - /*@ - @ loop assigns file_recovery->data_check; - @*/ + /*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */ + /*@ assert file_recovery->file_size <= PHOTOREC_MAX_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) {