src/file_emf.c: more frama-c annotations

1 files changed, 2 insertions, 0 deletions

diff --git a/src/file_emf.c b/src/file_emf.c
index 79f8752a..5bae67d8 100644
--- a/src/file_emf.c
+++ b/src/file_emf.c
@@ -208,6 +208,7 @@ struct EMF_HDR
   @ requires file_recovery->data_check==&data_check_emf;
   @ requires buffer_size >= 2;
   @ requires valid_data_check_param(buffer, buffer_size, file_recovery);
+  @ terminates \true;
   @ ensures  valid_data_check_result(\result, file_recovery);
   @ assigns file_recovery->calculated_file_size;
   @*/
@@ -217,6 +218,7 @@ static data_check_t data_check_emf(const unsigned char *buffer, const unsigned i
   /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
   /*@
     @ loop assigns file_recovery->calculated_file_size;
+    @ loop variant file_recovery->file_size + buffer_size/2 - (file_recovery->calculated_file_size + 8);
     @*/
   while(file_recovery->calculated_file_size + buffer_size/2  >= file_recovery->file_size &&
       file_recovery->calculated_file_size + 8 < file_recovery->file_size + buffer_size/2)