38 files changed, 237 insertions, 36 deletions
diff --git a/src/autoset.h b/src/autoset.h
index a7f512bf..b53832bc 100644
--- a/src/autoset.h
+++ b/src/autoset.h
@@ -28,6 +28,7 @@ extern "C" {
 /*@
   @ requires \valid(disk_car);
   @ requires valid_disk(disk_car);
+  @ terminates \true;
   @ assigns disk_car->unit;
   @*/
 void autoset_unit(disk_t *disk_car);
diff --git a/src/common.c b/src/common.c
index 7a21f49d..3b3a3cae 100644
--- a/src/common.c
+++ b/src/common.c
@@ -270,6 +270,7 @@ char* strip_dup(char* str)
 
 /*@
   @ requires 0 <= year <= 127;
+  @ terminates \true;
   @ ensures 0 <= \result <= 32;
   @ assigns \nothing;
   @*/
@@ -302,6 +303,7 @@ static unsigned int _date_get_leap_day(const unsigned long int year, const unsig
   @ requires 0 <= year <= 127;
   @ requires 0 <= leap_day <= 32;
   @ requires 0 <= day <= 30;
+  @ terminates \true;
   @ ensures 0 <= \result <= 334 + 127 * 365 + 32 + 30 + DAYS_DELTA;
   @ assigns \nothing;
   @*/
@@ -311,6 +313,7 @@ static unsigned long int _date_get_days(const unsigned long int days, const unsi
 }
 /*@
   @ requires 0 <= seconds2 <= 31;
+  @ terminates \true;
   @ ensures 0 <= \result <= 62;
   @ assigns \nothing;
   @*/
@@ -321,6 +324,7 @@ static unsigned long int _date_get_seconds(const unsigned long int seconds2)
 
 /*@
   @ requires 0 <= m <= 0x3f;
+  @ terminates \true;
   @ ensures 0 <= \result <= 0x3f * SECS_PER_MIN;
   @ assigns \nothing;
   @*/
@@ -331,6 +335,7 @@ static unsigned long int _date_min_to_seconds(const unsigned long int m)
 
 /*@
   @ requires 0 <= h <= 0x3f;
+  @ terminates \true;
   @ ensures 0 <= \result <= 0x3f * SECS_PER_HOUR;
   @ assigns \nothing;
   @*/
@@ -343,6 +348,7 @@ static unsigned long int _date_hours_to_seconds(const unsigned long int h)
   @ requires -14*3600 <= secwest <= 12*3600;
   @ requires f_time <= 0xffffffff;
   @ requires f_date <= 0xffffffff;
+  @ terminates \true;
   @ assigns \nothing;
   @*/
 time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
diff --git a/src/crc.c b/src/crc.c
index 8c8418a8..675e1144 100644
--- a/src/crc.c
+++ b/src/crc.c
@@ -92,8 +92,11 @@ unsigned int get_crc32(const void*buf, const unsigned int len, const uint32_t se
   const unsigned char *s=(const unsigned char *)buf;
   /*@ assert \valid_read(s + (0 .. len-1)); */
   crc32val = seed; 
-  /*@ loop invariant 0 <= i <= len;
-    @ loop assigns i, crc32val; */
+  /*@
+    @ loop invariant 0 <= i <= len;
+    @ loop assigns i, crc32val;
+    @ loop variant len - i;
+    @*/
   for (i = 0;  i < len;  i ++)
   {
     /*@ assert i < len; */
diff --git a/src/crc.h b/src/crc.h
index 50d651d4..a676232d 100644
--- a/src/crc.h
+++ b/src/crc.h
@@ -33,6 +33,7 @@ unsigned int get_crc32_gen(const unsigned char *s, const unsigned int len, const
 /*@
   @ requires \valid_read((const char *)s + (0 .. len-1));
   @ requires \initialized((const char *)s + (0 .. len-1));
+  @ terminates \true;
   @ assigns \nothing;
   @*/
 unsigned int get_crc32(const void *s, const unsigned int len, const uint32_t seed);
diff --git a/src/ext2_common.h b/src/ext2_common.h
index 40c630a1..8bef1a76 100644
--- a/src/ext2_common.h
+++ b/src/ext2_common.h
@@ -206,12 +206,14 @@ struct ext2_super_block {
 
 /*@
   @ requires \valid_read(super);
+  @ terminates \true;
   @ assigns  \nothing;
   @*/
 uint64_t td_ext2fs_blocks_count(const struct ext2_super_block *super);
 
 /*@
   @ requires \valid_read(super);
+  @ terminates \true;
   @ assigns  \nothing;
   @*/
 uint64_t td_ext2fs_free_blocks_count(const struct ext2_super_block *super);
@@ -221,6 +223,7 @@ uint64_t td_ext2fs_free_blocks_count(const struct ext2_super_block *super);
   @ requires \initialized(sb);
   @ requires partition==\null || (\valid_read(partition) && valid_partition(partition));
   @ requires \separated(sb, partition);
+  @ terminates \true;
   @ assigns  \nothing;
   @ ensures  \result == 7 ==> le32(sb->s_log_block_size) > 6;
   @ ensures  \result == 0 ==> le32(sb->s_log_block_size) <= 6;
diff --git a/src/fat_common.h b/src/fat_common.h
index 2b43e79f..d1c54ad2 100644
--- a/src/fat_common.h
+++ b/src/fat_common.h
@@ -137,6 +137,7 @@ struct msdos_dir_slot {
 /*@
   @ requires \valid_read(entry);
   @ requires \initialized(entry);
+  @ terminates \true;
   @ assigns \nothing;
   @ */
 unsigned int fat_get_cluster_from_entry(const struct msdos_dir_entry *entry);
@@ -150,6 +151,7 @@ int is_fat_directory(const unsigned char *buffer);
 /*@
   @ requires \valid_read(fat_header);
   @ requires \initialized(fat_header);
+  @ terminates \true;
   @ ensures \result <= 65535;
   @ assigns \nothing;
   @ */
@@ -158,6 +160,7 @@ unsigned int get_dir_entries(const struct fat_boot_sector *fat_header);
 /*@
   @ requires \valid_read(fat_header);
   @ requires \initialized(fat_header);
+  @ terminates \true;
   @ ensures \result <= 65535;
   @ assigns \nothing;
   @ */
@@ -166,6 +169,7 @@ unsigned int fat_sector_size(const struct fat_boot_sector *fat_header);
 /*@
   @ requires \valid_read(fat_header);
   @ requires \initialized(fat_header);
+  @ terminates \true;
   @ ensures \result <= 65535;
   @ assigns \nothing;
   @ */
diff --git a/src/fidentify.c b/src/fidentify.c
index 68403e36..06ba66cf 100644
--- a/src/fidentify.c
+++ b/src/fidentify.c
@@ -122,6 +122,7 @@ static data_check_t data_check_aux(file_recovery_t *file_recovery, const unsigne
     char *buffer=buffer_start+blocksize;
     unsigned int i;
     size_t lu=0;
+    /*@ assert valid_file_recovery(file_recovery); */
     memset(buffer, 0, READ_SIZE);
     lu=fread(buffer, 1, READ_SIZE, file_recovery->handle);
     if(lu <= 0)
diff --git a/src/file_dir.c b/src/file_dir.c
index 387b4e0c..9953959f 100644
--- a/src/file_dir.c
+++ b/src/file_dir.c
@@ -79,6 +79,7 @@ static void file_rename_fatdir(file_recovery_t *file_recovery)
   @ requires file_recovery->data_check == &data_check_fatdir;
   @ requires buffer_size >= 2;
   @ requires valid_data_check_param(buffer, buffer_size, file_recovery);
+  @ terminates \true;
   @ ensures  valid_data_check_result(\result, file_recovery);
   @ ensures \result == DC_STOP;
   @ assigns file_recovery->calculated_file_size;
diff --git a/src/file_flv.c b/src/file_flv.c
index 16128833..c05a3450 100644
--- a/src/file_flv.c
+++ b/src/file_flv.c
@@ -76,6 +76,7 @@ static data_check_t data_check_flv(const unsigned char *buffer, const unsigned i
   /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
   /*@
     @ loop assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp;
+    @ loop variant file_recovery->file_size + buffer_size/2 - (file_recovery->calculated_file_size + 15);
     @*/
   while(file_recovery->calculated_file_size + buffer_size/2  >= file_recovery->file_size &&
       file_recovery->calculated_file_size + 15 < file_recovery->file_size + buffer_size/2)
@@ -97,6 +98,7 @@ static data_check_t data_check_flv(const unsigned char *buffer, const unsigned i
 	file_recovery->calculated_file_size+=4;
 	return DC_STOP;
       }
+      /*@ assert file_recovery->data_check_tmp > 0; */
       /* 4+11=15*/
       file_recovery->calculated_file_size+=(uint64_t)15+file_recovery->data_check_tmp;
     }
diff --git a/src/file_gif.c b/src/file_gif.c
index cc529e29..54784ade 100644
--- a/src/file_gif.c
+++ b/src/file_gif.c
@@ -80,6 +80,7 @@ static void file_check_gif(file_recovery_t *file_recovery)
   @ requires file_recovery->data_check==&data_check_gif;
   @ requires valid_data_check_param(buffer, buffer_size, file_recovery);
   @ ensures  valid_data_check_result(\result, file_recovery);
+  @ ensures file_recovery->data_check == &data_check_gif || file_recovery->data_check == &data_check_gif2;
   @ assigns file_recovery->calculated_file_size, file_recovery->data_check;
   @*/
 static data_check_t data_check_gif(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
@@ -145,6 +146,7 @@ static data_check_t data_check_gif(const unsigned char *buffer, const unsigned i
   @ requires file_recovery->data_check==&data_check_gif2;
   @ requires valid_data_check_param(buffer, buffer_size, file_recovery);
   @ ensures  valid_data_check_result(\result, file_recovery);
+  @ ensures file_recovery->data_check == &data_check_gif || file_recovery->data_check == &data_check_gif2;
   @ assigns file_recovery->calculated_file_size, file_recovery->data_check;
   @*/
 static data_check_t data_check_gif2(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
@@ -152,6 +154,7 @@ static data_check_t data_check_gif2(const unsigned char *buffer, const unsigned
   /*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */
   /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
   /*@
+    @ loop invariant file_recovery->data_check == &data_check_gif || file_recovery->data_check == &data_check_gif2;
     @ loop assigns file_recovery->calculated_file_size, file_recovery->data_check;
     @ loop variant file_recovery->file_size + buffer_size/2 - (file_recovery->calculated_file_size + 1);
     @*/
@@ -159,6 +162,7 @@ static data_check_t data_check_gif2(const unsigned char *buffer, const unsigned
       file_recovery->calculated_file_size + 1 < file_recovery->file_size + buffer_size/2)
   {
     const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size;
+    /*@ assert file_recovery->data_check==&data_check_gif2; */
     /*@ assert 0 <= i < buffer_size - 1; */
 #ifdef DEBUG_GIF
     log_info("data_check_gif2 calculated_file_size=0x%llx\n",
@@ -173,7 +177,9 @@ static data_check_t data_check_gif2(const unsigned char *buffer, const unsigned
       file_recovery->data_check=&data_check_gif;
       return data_check_gif(buffer, buffer_size, file_recovery);
     }
+    /*@ assert file_recovery->data_check==&data_check_gif2; */
   }
+  /*@ assert file_recovery->data_check==&data_check_gif2; */
   return DC_CONTINUE;
 }
 
diff --git a/src/file_oci.c b/src/file_oci.c
index c21619ca..9a901b13 100644
--- a/src/file_oci.c
+++ b/src/file_oci.c
@@ -53,6 +53,7 @@ struct oci_header
 /*@
   @ requires file_recovery->data_check==&data_check_oci;
   @ 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;
   @*/
@@ -60,7 +61,10 @@ static data_check_t data_check_oci(const unsigned char *buffer, const unsigned i
 {
   /*@ 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; */
+  /*@
+    @ 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)
   {
@@ -99,6 +103,7 @@ static data_check_t data_check_oci(const unsigned char *buffer, const unsigned i
   @ requires buffer_size >= sizeof(struct oci_header);
   @ requires separation: \separated(&file_hint_oci, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
diff --git a/src/file_ogg.c b/src/file_ogg.c
index 1c9aa451..3133a39e 100644
--- a/src/file_ogg.c
+++ b/src/file_ogg.c
@@ -60,6 +60,7 @@ static data_check_t data_check_ogg(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 + 27 +255);
     @*/
   while(file_recovery->calculated_file_size + buffer_size/2  >= file_recovery->file_size &&
       file_recovery->calculated_file_size + 27 +255 < file_recovery->file_size + buffer_size/2)
@@ -76,6 +77,7 @@ static data_check_t data_check_ogg(const unsigned char *buffer, const unsigned i
       /*@
         @ loop invariant page_size <= 255 + 27 + j * 255;
         @ loop assigns j, page_size;
+	@ loop variant number_page_segments - j;
 	@ */
       for(j=0; j<number_page_segments; j++)
         page_size+=buffer[i+27+j];
diff --git a/src/file_par2.c b/src/file_par2.c
index 109e54a8..aa77c01d 100644
--- a/src/file_par2.c
+++ b/src/file_par2.c
@@ -59,7 +59,10 @@ static data_check_t data_check_par2(const unsigned char *buffer, const unsigned
 {
   /*@ 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; */
+  /*@
+    @ loop assigns file_recovery->calculated_file_size;
+    @ loop variant file_recovery->file_size + buffer_size/2 - (file_recovery->calculated_file_size + 16);
+    @*/
   while(file_recovery->calculated_file_size + buffer_size/2  >= file_recovery->file_size &&
       file_recovery->calculated_file_size + 16 < file_recovery->file_size + buffer_size/2)
   {
@@ -86,7 +89,10 @@ static void file_rename_par2(file_recovery_t *file_recovery)
   uint64_t offset=0;
   if((file=fopen(file_recovery->filename, "rb"))==NULL)
     return;
-  /*@ loop invariant valid_file_rename_param(file_recovery); */
+  /*@
+    @ loop invariant valid_file_rename_param(file_recovery);
+    @ loop variant PHOTOREC_MAX_FILE_SIZE - offset;
+    @*/
   while(offset <= PHOTOREC_MAX_FILE_SIZE)
   {
     uint64_t length;
@@ -111,6 +117,7 @@ static void file_rename_par2(file_recovery_t *file_recovery)
       fclose(file);
       return;
     }
+    /*@ assert length >= 16; */
     if(memcmp(&buffer[0x30], "PAR 2.0\0FileDesc", 16)==0)
     {
       fclose(file);
diff --git a/src/file_pdb.c b/src/file_pdb.c
index 31e42437..480907f3 100644
--- a/src/file_pdb.c
+++ b/src/file_pdb.c
@@ -46,6 +46,7 @@ const file_hint_t file_hint_pdb= {
 /*@
   @ requires file_recovery->data_check==&data_check_pdb;
   @ 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;
   @*/
@@ -54,7 +55,10 @@ static data_check_t data_check_pdb(const unsigned char *buffer, const unsigned i
   unsigned int i;
   /*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */
   /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
-  /*@ loop assigns i; */
+  /*@
+    @ loop assigns i;
+    @ loop variant buffer_size - i;
+    @*/
   for(i=buffer_size/2; i<buffer_size; i++)
     if(buffer[i]==0)
     {
@@ -93,6 +97,7 @@ static void file_check_pdb(file_recovery_t *file_recovery)
   @ requires buffer_size >= 70;
   @ requires separation: \separated(&file_hint_pdb, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
diff --git a/src/file_pdf.c b/src/file_pdf.c
index 128ebb1d..2a61bb89 100644
--- a/src/file_pdf.c
+++ b/src/file_pdf.c
@@ -58,6 +58,7 @@ const file_hint_t file_hint_pdf= {
 };
 
 /*@
+  @ terminates \true;
   @ assigns \nothing;
   @*/
 static int is_hexa(const int c)
@@ -66,6 +67,7 @@ static int is_hexa(const int c)
 }
 
 /*@
+  @ terminates \true;
   @ assigns \nothing;
   @ ensures 0 <= \result <= 15;
   @*/
@@ -145,6 +147,7 @@ static void file_rename_pdf(file_recovery_t *file_recovery)
   /*@
     @ loop invariant 0 <= i <= bsize;
     @ loop assigns i;
+    @ loop variant bsize - i;
     @ */
   for(i=0; i<bsize && buffer[i]==' '; i++);
   if(i + 2 >= bsize)
@@ -166,6 +169,7 @@ static void file_rename_pdf(file_recovery_t *file_recovery)
       @ loop invariant j <= s;
       @ loop invariant j <  bsize;
       @ loop assigns s, j, buffer[0 .. 512-1];
+      @ loop variant bsize - (s+1);
       @ */
     for(s=i+1, j=i+1;
 	s+1<bsize && is_hexa(buffer[s]) && is_hexa(buffer[s+1]);
@@ -188,6 +192,7 @@ static void file_rename_pdf(file_recovery_t *file_recovery)
         @ loop invariant l < i;
         @ loop invariant \initialized(title + (0 .. l-1));
         @ loop assigns i, l, title[0 .. 512-1];
+	@ loop variant bsize - i;
 	@*/
       while(i<bsize)
       {
@@ -209,6 +214,7 @@ static void file_rename_pdf(file_recovery_t *file_recovery)
         @ loop invariant l < i;
         @ loop invariant \initialized(title + (0 .. l-1));
         @ loop assigns i, l, title[0 .. 512-1];
+	@ loop variant bsize - (i+1);
 	@*/
       while(i+1 < bsize)
       {
@@ -226,6 +232,7 @@ static void file_rename_pdf(file_recovery_t *file_recovery)
         @ loop invariant l < i;
         @ loop invariant \initialized(title + (0 .. l-1));
         @ loop assigns i, l, title[0 .. 512-1];
+	@ loop variant bsize - i;
 	@*/
       while(i<bsize && buffer[i]!=')')
 	title[l++]=sbuffer[i++];
@@ -277,6 +284,7 @@ static void file_date_pdf(file_recovery_t *file_recovery)
     @ loop assigns offset, j, *file_recovery->handle, file_recovery->time, buffer[0..4095];
     @ loop assigns errno;
     @ loop assigns Frama_C_entropy_source;
+    @ loop variant file_recovery->file_size - offset;
     @*/
   while(offset < file_recovery->file_size)
   {
@@ -295,6 +303,7 @@ static void file_date_pdf(file_recovery_t *file_recovery)
       @ loop invariant 0 <= i <= bsize;
       @ loop assigns i, j, *file_recovery->handle, file_recovery->time, buffer[0..21];
       @ loop assigns errno;
+      @ loop variant bsize - i;
       @*/
     for(i=0; i<bsize; i++)
     {
@@ -363,7 +372,8 @@ static void file_check_pdf_and_size(file_recovery_t *file_recovery)
     @ loop assigns *file_recovery->handle, file_recovery->time;
     @ loop assigns errno;
     @ loop assigns Frama_C_entropy_source;
-  @*/
+    @ loop variant i;
+    @*/
   for(i=taille-4;i>=0;i--)
   {
     if(buffer[i]=='%' && buffer[i+1]=='E' && buffer[i+2]=='O' && buffer[i+3]=='F')
@@ -397,13 +407,17 @@ static void file_check_pdf(file_recovery_t *file_recovery)
 static uint64_t read_pdf_file_aux(const unsigned char *buffer, unsigned int i)
 {
   uint64_t file_size=0;
-  /*@ loop assigns i; */
+  /*@
+    @ loop assigns i;
+    @ loop variant 512 - i;
+    @*/
   while(i < 512 &&
       (buffer[i] ==' ' || buffer[i]=='\t' || buffer[i]=='\n' || buffer[i]=='\r'))
     i++;
   /*@
     @ loop invariant file_size <= PHOTOREC_MAX_FILE_SIZE;
     @ loop assigns i, file_size;
+    @ loop variant 512 - i;
     @ */
   for(;i<512 && buffer[i]>='0' && buffer[i]<='9'; i++)
   {
diff --git a/src/file_png.c b/src/file_png.c
index d1b9b164..10a349f5 100644
--- a/src/file_png.c
+++ b/src/file_png.c
@@ -78,6 +78,7 @@ struct png_ihdr
 /*@
   @ requires \valid_read(ihdr);
   @ requires \initialized(ihdr);
+  @ terminates \true;
   @ ensures  \result == 0 || \result == 1;
   @ assigns  \nothing;
   @ */
@@ -127,6 +128,7 @@ static void file_check_png(file_recovery_t *fr)
     @ loop invariant fr->file_size < 0x8000000000000000;
     @ loop assigns *fr->handle, errno, fr->file_size;
     @ loop assigns Frama_C_entropy_source;
+    @ loop variant 0x8000000000000000 - fr->file_size;
     @*/
   while(1)
   {
@@ -182,6 +184,7 @@ static data_check_t data_check_mng(const unsigned char *buffer, const unsigned i
   /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
   /*@
     @ loop assigns file_recovery->calculated_file_size, file_recovery->offset_ok;
+    @ 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)
@@ -221,6 +224,7 @@ static data_check_t data_check_png(const unsigned char *buffer, const unsigned i
   /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
   /*@
     @ loop assigns file_recovery->calculated_file_size, file_recovery->offset_ok;
+    @ 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)
diff --git a/src/file_ps.c b/src/file_ps.c
index 396c72ad..c8d5652f 100644
--- a/src/file_ps.c
+++ b/src/file_ps.c
@@ -63,6 +63,7 @@ static void file_check_ps(file_recovery_t *file_recovery)
   @ requires buffer_size > 8;
   @ requires file_recovery->data_check==&data_check_ps;
   @ 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;
   @*/
@@ -73,6 +74,7 @@ static data_check_t data_check_ps(const unsigned char *buffer, const unsigned in
   /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
   /*@
     @ loop assigns i, file_recovery->calculated_file_size;
+    @ loop variant buffer_size - (i+4);
     @*/
   for(i=(buffer_size/2)-4;i+4<buffer_size;i++)
   {
@@ -99,7 +101,10 @@ static int header_check_ps(const unsigned char *buffer, const unsigned int buffe
   reset_file_recovery(file_recovery_new);
   file_recovery_new->min_filesize=sizeof(ps_header);
   file_recovery_new->file_check=&file_check_ps;
-  /*@ loop assigns i, file_recovery_new->extension, file_recovery_new->data_check; */
+  /*@
+    @ loop assigns i, file_recovery_new->extension, file_recovery_new->data_check;
+    @ loop variant 20 - i;
+    @*/
   for(i=sizeof(ps_header); i < 20; i++)
   {
     switch(buffer[i])
diff --git a/src/file_psp.c b/src/file_psp.c
index e7041f25..c39ee500 100644
--- a/src/file_psp.c
+++ b/src/file_psp.c
@@ -62,6 +62,7 @@ static data_check_t data_check_psp(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 + 10);
     @*/
   while(file_recovery->calculated_file_size + buffer_size/2  >= file_recovery->file_size &&
       file_recovery->calculated_file_size + 10 < file_recovery->file_size + buffer_size/2)
diff --git a/src/file_qbb.c b/src/file_qbb.c
index ec6127b0..a020f4ee 100644
--- a/src/file_qbb.c
+++ b/src/file_qbb.c
@@ -96,7 +96,10 @@ static void file_rename_qbb(file_recovery_t *file_recovery)
   Frama_C_make_unknown(buffer, sizeof(buffer));
 #endif
   /*@ assert \valid_read((char *)&buffer + (0 .. lu-1)); */
-  /*@ loop assigns i; */
+  /*@
+    @ loop assigns i;
+    @ loop variant lu - (i+sizeof(struct qbb_header02));
+    @*/
   while(i+sizeof(struct qbb_header02) <= lu)
   {
     /*@ assert i+sizeof(struct qbb_header02) <= lu; */
@@ -140,6 +143,7 @@ static int header_check_qbb(const unsigned char *buffer, const unsigned int buff
     return 0;
   /*@
     @ loop assigns i, data_size;
+    @ loop variant buffer_size - (i+sizeof(struct qbb_header02));
     @*/
   while(i+sizeof(struct qbb_header02) < buffer_size)
   {
@@ -178,6 +182,7 @@ static int header_check_qbb(const unsigned char *buffer, const unsigned int buff
   @ requires buffer_size >= 0x64;
   @ requires separation: \separated(&file_hint_qbb, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
diff --git a/src/file_r3d.c b/src/file_r3d.c
index 9a8007af..78d2f81f 100644
--- a/src/file_r3d.c
+++ b/src/file_r3d.c
@@ -55,6 +55,7 @@ struct atom_struct
 /*@
   @ requires file_recovery->data_check==&data_check_r3d;
   @ 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, file_recovery->data_check;
   @*/
@@ -64,6 +65,7 @@ static data_check_t data_check_r3d(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)
   {
@@ -119,7 +121,10 @@ static void file_rename_r3d(file_recovery_t *file_recovery)
   fclose(file);
   if(buffer_size < 0x44)
     return;
-  /*@ loop assigns i; */
+  /*@
+    @ loop assigns i;
+    @ loop variant buffer_size - i;
+    @*/
   for(i = 0x43; i < buffer_size && buffer[i] != 0 && buffer[i] != '.'; i++)
   {
     if(!isalnum(buffer[i]) && buffer[i] != '_')
@@ -132,6 +137,7 @@ static void file_rename_r3d(file_recovery_t *file_recovery)
   @ requires buffer_size >= sizeof(struct atom_struct);
   @ requires separation: \separated(&file_hint_r3d, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
@@ -158,6 +164,7 @@ static int header_check_r3d(const unsigned char *buffer, const unsigned int buff
   @ requires buffer_size >= 0xc;
   @ requires separation: \separated(&file_hint_r3d, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
diff --git a/src/file_spf.c b/src/file_spf.c
index 1fd1d832..a2c8219e 100644
--- a/src/file_spf.c
+++ b/src/file_spf.c
@@ -60,8 +60,11 @@ static void file_check_spf(file_recovery_t *file_recovery)
   {
     return;
   }
-  /*@ loop assigns *file_recovery->handle, file_recovery->file_size;
-    @ loop assigns Frama_C_entropy_source, errno; */
+  /*@
+    @ loop invariant valid_file_check_param(file_recovery);
+    @ loop assigns *file_recovery->handle, file_recovery->file_size;
+    @ loop assigns Frama_C_entropy_source, errno;
+    @*/
   while(1)
   {
     int i;
@@ -75,7 +78,11 @@ static void file_check_spf(file_recovery_t *file_recovery)
 #ifdef __FRAMAC__
     Frama_C_make_unknown(buffer, READ_SIZE);
 #endif
-    /*@ loop assigns i, file_recovery->file_size; */
+    /*@
+      @ loop invariant valid_file_check_param(file_recovery);
+      @ loop assigns i, file_recovery->file_size;
+      @ loop variant PHOTOREC_MAX_FILE_SIZE - file_recovery->file_size;
+      @*/
     for(i=0; i<taille; i+=512)
     {
       int j;
@@ -85,11 +92,17 @@ static void file_check_spf(file_recovery_t *file_recovery)
       {
 	return;
       }
-      /*@ loop assigns j, is_valid; */
+      /*@
+        @ loop assigns j, is_valid;
+	@ loop variant 8 - j;
+	@*/
       for(j=0; j<8; j++)
 	if(buffer[i+j]!=0)
 	  is_valid=1;
-      /*@ loop assigns j; */
+      /*@
+        @ loop assigns j;
+	@ loop variant 512 - j;
+	@*/
       for(j=8; j<512 && buffer[i+j]==0; j++);
       if(is_valid > 0 && j==512)
       {
diff --git a/src/file_stl.c b/src/file_stl.c
index cb312a82..6323ec54 100644
--- a/src/file_stl.c
+++ b/src/file_stl.c
@@ -48,6 +48,7 @@ const file_hint_t file_hint_stl= {
   @ requires buffer_size >= 84;
   @ requires separation: \separated(&file_hint_stl, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
@@ -59,11 +60,17 @@ static int header_check_stl(const unsigned char *buffer, const unsigned int buff
   const uint32_t *fs_ptr=(const uint32_t *)&buffer[80];
   const uint64_t filesize=80+4+(uint64_t)le32(*fs_ptr)*50;
   /*@ assert filesize < PHOTOREC_MAX_FILE_SIZE; */
-  /*@ loop assigns i; */
+  /*@
+    @ loop assigns i;
+    @ loop variant 80 - i;
+    @*/
   for(i=0; i<80 && buffer[i]!='\0'; i++);
   if(i>64)
     return 0;
-  /*@ loop assigns i; */
+  /*@
+    @ loop assigns i;
+    @ loop variant 80 - i;
+    @*/
   for(i++; i<80 && buffer[i]==' '; i++);
   if(i!=80)
     return 0;
diff --git a/src/file_swf.c b/src/file_swf.c
index 6ab0fe08..4b7ac521 100644
--- a/src/file_swf.c
+++ b/src/file_swf.c
@@ -84,6 +84,7 @@ struct swfz_header
   @ requires 0 <= *offset_bit <= 7;
   @ requires 2 <= nbit <= 31;
   @ requires separation: \separated(data, offset_bit, *data + (0..(nbit+*offset_bit)/8));
+  @ terminates \true;
   @ ensures  0 <= *offset_bit <= 7;
   @ assigns *data, *offset_bit;
   @*/
@@ -119,6 +120,7 @@ static int read_SB(const unsigned char **data, unsigned int *offset_bit, unsigne
   @ requires buffer_size >= 512;
   @ requires separation: \separated(&file_hint_swf, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
   @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size_max);
@@ -202,6 +204,7 @@ static int header_check_swfc(const unsigned char *buffer, const unsigned int buf
   @ requires buffer_size >= sizeof(struct swf_header);
   @ requires separation: \separated(&file_hint_swf, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
   @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@@ -246,6 +249,7 @@ static int header_check_swf(const unsigned char *buffer, const unsigned int buff
   @ requires buffer_size >= sizeof(struct swfz_header);
   @ requires separation: \separated(&file_hint_swf, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
   @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size_max);
diff --git a/src/file_tar.c b/src/file_tar.c
index 3098e049..89a1ea30 100644
--- a/src/file_tar.c
+++ b/src/file_tar.c
@@ -49,6 +49,7 @@ const file_hint_t file_hint_tar = {
 
 /*@
   @ requires \valid_read(h);
+  @ terminates \true;
   @ assigns \nothing;
   @*/
 static int is_valid_checksum_format(const struct tar_posix_header *h)
@@ -59,6 +60,7 @@ static int is_valid_checksum_format(const struct tar_posix_header *h)
   /* No checksum ? */
   /*@
     @ loop assigns i,all_null;
+    @ loop variant 8 - i;
     @*/
   for(i = 0; i < 8; i++)
     if(h->chksum[i] != 0)
@@ -71,6 +73,7 @@ static int is_valid_checksum_format(const struct tar_posix_header *h)
    */
   /*@
     @ loop assigns i,space_allowed;
+    @ loop variant 6 - i;
     @*/
   for(i = 0; i < 6; i++)
   {
diff --git a/src/file_tib.c b/src/file_tib.c
index 53b1099f..47466359 100644
--- a/src/file_tib.c
+++ b/src/file_tib.c
@@ -59,7 +59,10 @@ static data_check_t data_check_tib2(const unsigned char *buffer, const unsigned
 {
   /*@ 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; */
+  /*@
+    @ loop assigns file_recovery->calculated_file_size;
+    @ loop variant file_recovery->file_size + buffer_size/2 - (file_recovery->calculated_file_size + 512);
+    @*/
   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)
   {
@@ -109,6 +112,7 @@ static void file_check_tib2(file_recovery_t *file_recovery)
 /*@
   @ loop assigns *file_recovery->handle, errno, file_size;
   @ loop assigns Frama_C_entropy_source;
+  @ loop variant file_size;
   @*/
   for(; file_size>0; file_size-=512)
   {
@@ -120,7 +124,10 @@ static void file_check_tib2(file_recovery_t *file_recovery)
       file_recovery->file_size=0;
       return;
     }
-    /*@ loop assigns i; */
+    /*@
+      @ loop assigns i;
+      @ loop variant 512 - i;
+      @*/
     for(i=0; i<512 && buffer[i]==0; i++);
     if(i!=512)
     {
@@ -133,6 +140,7 @@ static void file_check_tib2(file_recovery_t *file_recovery)
 /*@
   @ requires separation: \separated(&file_hint_tib, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
@@ -146,6 +154,7 @@ static int header_check_tib(const unsigned char *buffer, const unsigned int buff
 /*@
   @ requires separation: \separated(&file_hint_tib, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
diff --git a/src/file_ttf.c b/src/file_ttf.c
index 897e9c2b..882c8904 100644
--- a/src/file_ttf.c
+++ b/src/file_ttf.c
@@ -66,6 +66,7 @@ struct ttf_table_directory
 };
 
 /*@
+  @ terminates \true;
   @ assigns \nothing;
   @*/
 static unsigned int td_ilog2(unsigned int v)
@@ -74,6 +75,7 @@ static unsigned int td_ilog2(unsigned int v)
   /*@
     @ loop assigns v,l;
     @ loop unroll 16;
+    @ loop variant v;
     @*/
   while(v >>= 1)
     l++;
@@ -84,6 +86,7 @@ static unsigned int td_ilog2(unsigned int v)
   @ requires buffer_size >= sizeof(struct ttf_offset_table);
   @ requires separation: \separated(&file_hint_ttf, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
@@ -122,6 +125,7 @@ static int header_check_ttf(const unsigned char *buffer, const unsigned int buff
     /*@ assert \valid_read(ttf_dir + (0 .. numTables -1)); */
     /*@
       @ loop assigns i, max_offset;
+      @ loop variant numTables - i;
       @*/
     for(i=0; i<numTables; i++)
     {
diff --git a/src/file_txt.c b/src/file_txt.c
index 15e73b22..5b1e19ce 100644
--- a/src/file_txt.c
+++ b/src/file_txt.c
@@ -348,6 +348,7 @@ static int filtre(unsigned int car)
 /*@
   @ requires \valid_read(buffer+(0..buffer_size-1));
   @ requires \initialized(buffer+(0..buffer_size-1));
+  @ terminates \true;
   @ assigns \nothing;
   @*/
 static int has_newline(const char *buffer, const unsigned int buffer_size)
@@ -370,6 +371,7 @@ static int has_newline(const char *buffer, const unsigned int buffer_size)
 /*@
   @ requires buffer_size > 0;
   @ requires \valid_read(buffer+(0..buffer_size-1));
+  @ terminates \true;
   @ assigns \nothing;
   @*/
 static unsigned int is_csv(const char *buffer, const unsigned int buffer_size)
@@ -479,6 +481,7 @@ static int is_ini(const unsigned char *buffer)
   @ requires buffer_size >= 0;
   @ requires \valid_read(buffer+(0..buffer_size-1));
   @ requires \initialized(buffer+(0..buffer_size-1));
+  @ terminates \true;
   @ assigns  \nothing;
   @*/
 static double is_random(const unsigned char *buffer, const unsigned int buffer_size)
@@ -701,6 +704,7 @@ static data_check_t data_check_html(const unsigned char *buffer, const unsigned
     unsigned int j;
     /*@
       @ loop assigns j, file_recovery->calculated_file_size;
+      @ loop variant buffer_size - (j+sizeof(sign_html_end)-1);
       @*/
     for(j=buffer_size/2-(sizeof(sign_html_end)-1);
 	j+sizeof(sign_html_end)-1 < buffer_size;
@@ -710,7 +714,10 @@ static data_check_t data_check_html(const unsigned char *buffer, const unsigned
       {
 	j+=sizeof(sign_html_end)-1;
 	/*@ assert j >= buffer_size/2; */
-	/*@ loop assigns j; */
+	/*@
+	  @ loop assigns j;
+	  @ loop variant buffer_size - j;
+	  @*/
 	while(j < buffer_size && (buffer[j]=='\n' || buffer[j]=='\r'))
 	  j++;
 	file_recovery->calculated_file_size+=j-buffer_size/2;
@@ -734,6 +741,7 @@ static data_check_t data_check_html(const unsigned char *buffer, const unsigned
 /*@
   @ requires file_recovery->data_check == &data_check_ttd;
   @ 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;
   @*/
@@ -760,6 +768,7 @@ static data_check_t data_check_ttd(const unsigned char *buffer, const unsigned i
 /*@
   @ requires file_recovery->data_check == &data_check_txt;
   @ 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;
   @*/
@@ -780,6 +789,7 @@ static data_check_t data_check_txt(const unsigned char *buffer, const unsigned i
   @ requires file_recovery->data_check == &data_check_xml_utf8;
   @ requires buffer_size >= 10;
   @ requires valid_data_check_param(buffer, buffer_size, file_recovery);
+  @ terminates \true;
   @ ensures  valid_data_check_result(\result, file_recovery);
   @ ensures \result == DC_CONTINUE ==> (file_recovery->data_check==&data_check_txt);
   @ assigns file_recovery->calculated_file_size,file_recovery->data_check;
@@ -1251,7 +1261,10 @@ static int header_check_mbox(const unsigned char *buffer, const unsigned int buf
       file_recovery->file_stat->file_hint==&file_hint_fasttxt &&
       file_recovery->extension==extension_mbox)
     return 0;
-  /*@ loop assigns i; */
+  /*@
+    @ loop assigns i;
+    @ loop variant 64 - i;
+    @*/
   for(i=0; i<64; i++)
     if(buffer[i]==0)
       return 0;
@@ -1259,7 +1272,10 @@ static int header_check_mbox(const unsigned char *buffer, const unsigned int buf
       memcmp(buffer, "From MAILER-DAEMON ", 19)!=0)
   {
     /* From someone@somewhere */
-    /*@ loop assigns i; */
+    /*@
+      @ loop assigns i;
+      @ loop variant 200 - i;
+      @*/
     for(i=5; i<200 && buffer[i]!=' ' && buffer[i]!='@'; i++);
     if(buffer[i]!='@')
       return 0;
@@ -1315,7 +1331,10 @@ static int header_check_perlm(const unsigned char *buffer, const unsigned int bu
   const unsigned int buffer_size_test=(buffer_size < 2048 ? buffer_size : 2048);
   if(buffer_size < 128)
     return 0;
-  /*@ loop assigns i; */
+  /*@
+    @ loop assigns i;
+    @ loop variant 128 - i;
+    */
   for(i=0; i<128 && buffer[i]!=';' && buffer[i]!='\n'; i++);
   if(buffer[i]!=';')
     return 0;
@@ -1357,7 +1376,10 @@ static int header_check_rtf(const unsigned char *buffer, const unsigned int buff
   unsigned int i;
   if(buffer_size < 16)
     return 0;
-  /*@ loop assigns i; */
+  /*@
+    @ loop assigns i;
+    @ loop variant 16 - i;
+    @*/
   for(i=0; i<16; i++)
     if(buffer[i]=='\0')
       return 0;
@@ -1509,7 +1531,10 @@ static int header_check_thunderbird(const unsigned char *buffer, const unsigned
       file_recovery->file_stat->file_hint==&file_hint_fasttxt &&
       file_recovery->extension == extension_mbox)
     return 0;
-  /*@ loop assigns i; */
+  /*@
+    @ loop assigns i;
+    @ loop variant 64 - i;
+    @*/
   for(i=0; i<64; i++)
     if(buffer[i]==0)
       return 0;
@@ -2245,9 +2270,15 @@ static void register_header_check_snz(file_stat_t *file_stat)
 static void register_header_check_txt(file_stat_t *file_stat)
 {
   unsigned int i;
-  /*@ loop assigns i, ascii_char[0 .. 255]; */
+  /*@
+    @ loop assigns i, ascii_char[0 .. 255];
+    @ loop variant 256 - i;
+    @*/
   for(i=0; i<256; i++)
     ascii_char[i]=i;
+  /*@
+    @ loop variant 256 - i;
+    @*/
   for(i=0; i<256; i++)
   {
     if(filtre(i) || i==0xE2 || i==0xC2 || i==0xC3 || i==0xC5 || i==0xC6 || i==0xCB)
diff --git a/src/file_vault.c b/src/file_vault.c
index 4b659731..eafa692e 100644
--- a/src/file_vault.c
+++ b/src/file_vault.c
@@ -53,6 +53,7 @@ const file_hint_t file_hint_vault = {
   @ requires buffer_size >= 2*29;
   @ requires file_recovery->data_check==&data_check_vault;
   @ 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;
   @*/
@@ -61,7 +62,10 @@ static data_check_t data_check_vault(const unsigned char *buffer, const unsigned
   unsigned int i;
   /*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */
   /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
-  /*@ loop assigns i, file_recovery->calculated_file_size; */
+  /*@
+    @ loop assigns i, file_recovery->calculated_file_size;
+    @ loop variant buffer_size - (i + 29);
+    @*/
   for(i = (buffer_size / 2) - 28; i + 29 <= buffer_size; i++)
   {
     if(buffer[i] == '-' && buffer[i + 5] == '-' && buffer[i + 10] == '-' && buffer[i + 15] == '-' && buffer[i + 28] == '\0')
@@ -77,6 +81,7 @@ static data_check_t data_check_vault(const unsigned char *buffer, const unsigned
 /*@
   @ requires separation: \separated(&file_hint_vault, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
diff --git a/src/file_wv.c b/src/file_wv.c
index 5debef9f..7f108e5f 100644
--- a/src/file_wv.c
+++ b/src/file_wv.c
@@ -75,7 +75,10 @@ static data_check_t data_check_wv(const unsigned char *buffer, const unsigned in
 {
   /*@ 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; */
+  /*@
+    @ loop assigns file_recovery->calculated_file_size;
+    @ loop variant file_recovery->file_size + buffer_size / 2 - (file_recovery->calculated_file_size + 16);
+    @*/
   while(file_recovery->calculated_file_size + buffer_size / 2 >= file_recovery->file_size && file_recovery->calculated_file_size + 16 <= file_recovery->file_size + buffer_size / 2)
   {
     const unsigned int i = file_recovery->calculated_file_size + buffer_size / 2 - file_recovery->file_size;
@@ -88,6 +91,7 @@ static data_check_t data_check_wv(const unsigned char *buffer, const unsigned in
     else if(buffer[i] == 'A' && buffer[i + 1] == 'P' && buffer[i + 2] == 'E' && buffer[i + 3] == 'T' && buffer[i + 4] == 'A' && buffer[i + 5] == 'G' && buffer[i + 6] == 'E' && buffer[i + 7] == 'X')
     { /* APE Tagv2 (APE Tagv1 has no header) http://wiki.hydrogenaudio.org/index.php?title=APE_Tags_Header */
       const uint64_t ape_tag_size = (buffer[i + 12] + (buffer[i + 13] << 8) + (buffer[i + 14] << 16) + ((uint64_t)buffer[i + 15] << 24)) + 32;
+      /*@ assert ape_tag_size > 0; */
       file_recovery->calculated_file_size += ape_tag_size;
     }
     else if(buffer[i] == 'T' && buffer[i + 1] == 'A' && buffer[i + 2] == 'G')
@@ -110,6 +114,7 @@ static data_check_t data_check_wv(const unsigned char *buffer, const unsigned in
   @ requires buffer_size >= sizeof(WavpackHeader);
   @ requires separation: \separated(&file_hint_wv, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
diff --git a/src/file_x4a.c b/src/file_x4a.c
index 9c6f463d..3370c5bb 100644
--- a/src/file_x4a.c
+++ b/src/file_x4a.c
@@ -70,6 +70,7 @@ static void file_check_x4a(file_recovery_t *fr)
 #endif
   /*@
     @ loop assigns i, fs;
+    @ loop variant 0x200 - i;
     @*/
   for(i = 0x80; i < 0x200; i += 8)
   {
diff --git a/src/file_xm.c b/src/file_xm.c
index f78a76ef..dd7d2c4e 100644
--- a/src/file_xm.c
+++ b/src/file_xm.c
@@ -66,6 +66,7 @@ static int parse_patterns(file_recovery_t *fr, uint16_t patterns)
     @ loop assigns *fr->handle, errno, fr->file_size;
     @ loop assigns Frama_C_entropy_source;
     @ loop assigns patterns;
+    @ loop variant patterns;
     @*/
   for(; patterns != 0; patterns--)
   {
@@ -123,6 +124,7 @@ static int parse_instruments(file_recovery_t *fr, uint16_t instrs)
     @ loop assigns *fr->handle, errno, fr->file_size;
     @ loop assigns Frama_C_entropy_source;
     @ loop assigns instrs;
+    @ loop variant instrs;
     @*/
   for(; instrs != 0; instrs--)
   {
@@ -180,7 +182,10 @@ static int parse_instruments(file_recovery_t *fr, uint16_t instrs)
       if(fseek(fr->handle, 234, SEEK_CUR) == -1)
         return -1;
 
-      /*@ loop assigns samples, size, *fr->handle, errno, Frama_C_entropy_source, fr->file_size, buffer[0..3]; */
+      /*@
+        @ loop assigns samples, size, *fr->handle, errno, Frama_C_entropy_source, fr->file_size, buffer[0..3];
+	@ loop variant samples;
+	@*/
       for(; samples != 0; samples--)
       {
         if(fread(&buffer, sizeof(uint32_t), 1, fr->handle) != 1)
@@ -261,6 +266,7 @@ static void file_check_xm(file_recovery_t *fr)
 /*@
   @ requires separation: \separated(&file_hint_xm, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
diff --git a/src/file_xml.c b/src/file_xml.c
index 12711aef..92826536 100644
--- a/src/file_xml.c
+++ b/src/file_xml.c
@@ -59,6 +59,7 @@ static void file_rename_xml_aux(file_recovery_t *file_recovery, const char *titl
   /*@
     @ loop invariant j <= size;
     @ loop assigns j;
+    @ loop variant size - 1 - j;
     @*/
   for(j = 0; j < size-1; j += 2)
   {
@@ -100,6 +101,7 @@ static void file_rename_xml(file_recovery_t *file_recovery)
   /*@
     @ loop invariant 0 <= i <= lu - 20 + 1;
     @ loop assigns i;
+    @ loop variant lu - 20 - i;
     @*/
   for(i = 0; i < lu - 20 && !(buffer[i] == 0 && buffer[i + 1] == 0); i += 2)
   {
@@ -116,6 +118,7 @@ static void file_rename_xml(file_recovery_t *file_recovery)
 /*@
   @ requires separation: \separated(&file_hint_xml, buffer+(..), file_recovery, file_recovery_new);
   @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ terminates \true;
   @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
   @*/
diff --git a/src/file_zip.c b/src/file_zip.c
index c12dfcc2..1939a752 100644
--- a/src/file_zip.c
+++ b/src/file_zip.c
@@ -1247,6 +1247,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
       fclose(fr.handle);
       /*@
         @ loop assigns len;
+	@ loop variant 32 - len;
 	@*/
       for(len=0; len<32 &&
 	  first_filename[len]!='\0' &&
diff --git a/src/filegen.c b/src/filegen.c
index ead3d6cf..477f6872 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -516,6 +516,7 @@ file_stat_t * init_file_stats(file_enable_t *files_enable)
   /*@ loop assigns enable_count, file_enable; */
   for(file_enable=files_enable;file_enable->file_hint!=NULL;file_enable++)
   {
+    /*@ assert \valid_read(file_enable); */
     if(file_enable->enable>0 && file_enable->file_hint->register_header_check!=NULL)
     {
       enable_count++;
@@ -526,15 +527,18 @@ file_stat_t * init_file_stats(file_enable_t *files_enable)
   i=0;
   /*@
     @ loop invariant 0 <= i <= enable_count;
+    @ loop invariant \forall integer j; 0 <= j < i ==> valid_file_stat(&file_stats[j]);
     @*/
   for(file_enable=files_enable;file_enable->file_hint!=NULL;file_enable++)
   {
+    /*@ assert \valid_read(file_enable); */
     if(file_enable->enable>0 && file_enable->file_hint->register_header_check!=NULL)
     {
       file_stats[i].file_hint=file_enable->file_hint;
       file_stats[i].not_recovered=0;
       file_stats[i].recovered=0;
       file_enable->file_hint->register_header_check(&file_stats[i]);
+      /*@ assert valid_file_stat(&file_stats[i]); */
       i++;
     }
   }
@@ -562,6 +566,7 @@ static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
   char *dst;
   char *dst_dir_sep;
   /*@ assert strlen((char *)&file_recovery->filename) < 2048; */
+  /*@ assert strlen(new_ext) < (1<<30); */
   const unsigned int len=strlen(file_recovery->filename)+1+strlen(new_ext)+1;
   /*@ assert valid_read_string(&file_recovery->filename[0]); */
   if(len > sizeof(file_recovery->filename))
@@ -610,6 +615,7 @@ static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
     dst++;
   /* Add extension */
   *dst++ = '.';
+  /*@ assert strlen(new_ext) < (1<<30); */
 #ifdef DISABLED_FOR_FRAMAC
   memcpy(dst, new_ext, strlen(new_ext)+1);
 #else
diff --git a/src/filegen.h b/src/filegen.h
index d3d6dbd3..74320f64 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -117,6 +117,10 @@ typedef struct
 } file_check_t;
 
 /*@
+   predicate valid_file_hint(file_hint_t *file_hint) = (\valid_read(file_hint) && valid_read_string(file_hint->description));
+
+   predicate valid_file_stat(file_stat_t *file_stat) = (\valid_read(file_stat) && valid_file_hint(file_stat->file_hint));
+
    predicate valid_file_check_node(file_check_t *node) = (\valid_read(node) &&
      \initialized(&node->offset) &&
      \initialized(&node->length) &&
@@ -125,7 +129,8 @@ typedef struct
      node->offset + node->length <= PHOTOREC_MAX_SIG_OFFSET &&
      \valid_read((const char *)node->value+(0..node->length-1)) &&
      \valid_function(node->header_check) &&
-     \valid(node->file_stat)
+     \valid(node->file_stat) &&
+     valid_file_stat(node->file_stat)
    );
    @*/
 
@@ -141,10 +146,6 @@ typedef struct
 #define NL_BARECR       (1 << 2)
 
 /*@
-   predicate valid_file_hint(file_hint_t *file_hint) = (\valid_read(file_hint) && valid_read_string(file_hint->description));
-
-   predicate valid_file_stat(file_stat_t *file_stat) = (\valid_read(file_stat) && valid_file_hint(file_stat->file_hint));
-
    predicate valid_file_recovery(file_recovery_t *file_recovery) = (\valid_read(file_recovery) &&
 	strlen((const char*)file_recovery->filename) < 1<<30 &&
         valid_read_string((const char *)file_recovery->filename) &&
@@ -224,7 +225,8 @@ typedef struct
     );
 
     predicate valid_register_header_check(file_stat_t *file_stat) = (
-	\valid(file_stat)
+	\valid(file_stat) &&
+	valid_file_stat(file_stat)
     );
   @*/
 void free_header_check(void);
@@ -361,6 +363,7 @@ void reset_file_recovery(file_recovery_t *file_recovery);
   @ requires \valid_read((const char *)value+(0..length-1));
   @ requires \valid_function(header_check);
   @ requires \valid(file_stat);
+  @ requires valid_file_stat(file_stat);
   @ ensures  \valid_read((const char *)value+(0..length-1));
   @*/
 void register_header_check(const unsigned int offset, const void *value, const unsigned int length,
@@ -370,6 +373,7 @@ void register_header_check(const unsigned int offset, const void *value, const u
 
 /*@
   @ requires \valid(files_enable);
+  @ ensures valid_file_stat(\result);
   @*/
 file_stat_t * init_file_stats(file_enable_t *files_enable);
 
@@ -395,6 +399,9 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
   @*/
 int file_rename_unicode(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int force_ext);
 
+/*@
+  @ terminates \true;
+  @*/
 void header_ignored_cond_reset(uint64_t start, uint64_t end);
 
 /*@
diff --git a/src/unicode.c b/src/unicode.c
index b499ac2b..304cb3b6 100644
--- a/src/unicode.c
+++ b/src/unicode.c
@@ -31,6 +31,10 @@
 int UCSle2str(char *to, const uint16_t *from, const unsigned int len)
 {
   unsigned int i;
+  /*@
+    @ loop assigns i, to[0 .. i];
+    @ loop variant len - i;
+    @*/
   for (i = 0; i < len && le16(from[i])!=0; i++)
   {
     if (le16(from[i]) & 0xff00)
@@ -46,6 +50,10 @@ int UCSle2str(char *to, const uint16_t *from, const unsigned int len)
 int str2UCSle(uint16_t *to, const char *from, const unsigned int len)
 {
   unsigned int i;
+  /*@
+    @ loop assigns i, to[0 .. i];
+    @ loop variant len - i;
+    @*/
   for (i = 0; (i < len) && from[i]; i++)
   {
     to[i] = le16(from[i]);
diff --git a/src/unicode.h b/src/unicode.h
index 22d2ccff..5384029c 100644
--- a/src/unicode.h
+++ b/src/unicode.h
@@ -29,6 +29,8 @@ extern "C" {
   @ requires \valid(to + ( 0 .. len-1));
   @ requires \valid_read(from + ( 0 .. len-1));
   @ requires \separated(to + (..), from + (..));
+  @ terminates \true;
+  @ assigns to[0 .. len-1];
   @*/
 int UCSle2str(char *to, const uint16_t *from, const unsigned int len);
 
@@ -36,6 +38,8 @@ int UCSle2str(char *to, const uint16_t *from, const unsigned int len);
   @ requires \valid(to + ( 0 .. len-1));
   @ requires \valid_read(from + ( 0 .. len-1));
   @ requires \separated(to + (..), from + (..));
+  @ terminates \true;
+  @ assigns to[0 .. len-1];
   @*/
 int str2UCSle(uint16_t *to, const char *from, const unsigned int len);
 
diff --git a/src/utfsize.h b/src/utfsize.h
index 205b652a..388148c0 100644
--- a/src/utfsize.h
+++ b/src/utfsize.h
@@ -28,6 +28,7 @@ extern "C" {
 /*@
   @ requires buf_len> 0;
   @ requires \valid_read(buffer+(0..buf_len-1));
+  @ terminates \true;
   @ ensures 0 <= \result <= buf_len;
   @ assigns \nothing;
   @*/