diff --git a/src/file_hdf.c b/src/file_hdf.c
index 233bf4e1..f6dc6991 100644
--- a/src/file_hdf.c
+++ b/src/file_hdf.c
@@ -65,48 +65,56 @@ struct dd_struct
 } __attribute__ ((gcc_struct, __packed__));
 
 /*@
-  @ requires \separated(file_recovery, file_recovery->handle, &errno, &Frama_C_entropy_source, &__fc_heap_status);
-  @ requires valid_file_check_param(file_recovery);
-  @ ensures  valid_file_check_result(file_recovery);
+  @ requires \valid(handle);
+  @ requires \valid(dd_buf + (0 .. 65536 * sizeof(struct dd_struct)-1));
+  @ requires \separated(handle, dd_buf + (..), &errno, &Frama_C_entropy_source);
+  @ assigns *(dd_buf + (0 .. 65536 * sizeof(struct dd_struct)-1));
+  @ assigns Frama_C_entropy_source;
+  @ assigns *handle, errno;
   @*/
-static void file_check_hdf(file_recovery_t *file_recovery)
+static uint64_t file_check_hdf_aux(FILE *handle, char *dd_buf)
 {
   uint64_t file_size=0;
   uint64_t offset_old;
   uint64_t offset=4;
-  struct dd_struct *dd=(struct dd_struct *)MALLOC(sizeof(struct dd_struct)*65536);
+  const struct dd_struct *dd=(const struct dd_struct *)dd_buf;
+  /*@
+    @ loop assigns file_size, offset_old, offset;
+    @ loop assigns *(dd_buf + (0 .. 65536 * sizeof(struct dd_struct)-1));
+    @ loop assigns Frama_C_entropy_source;
+    @ loop assigns *handle, errno;
+    @*/
   do
   {
-    struct ddh_struct ddh;
+    char ddh_buf[sizeof(struct ddh_struct)];
+    const struct ddh_struct *ddh=(const struct ddh_struct *)&ddh_buf;
     unsigned int i;
     unsigned int size;
-    if(my_fseek(file_recovery->handle, offset, SEEK_SET) < 0 ||
-	fread(&ddh, sizeof(ddh), 1, file_recovery->handle) !=1)
+    if(my_fseek(handle, offset, SEEK_SET) < 0 ||
+	fread(&ddh_buf, sizeof(ddh_buf), 1, handle) !=1)
     {
-      free(dd);
-      file_recovery->file_size=0;
-      return ;
+      return 0;
     }
 #ifdef __FRAMAC__
-    Frama_C_make_unknown(&ddh, sizeof(ddh));
+    Frama_C_make_unknown(&ddh_buf, sizeof(ddh_buf));
 #endif
-    size=be16(ddh.size);
+    size=be16(ddh->size);
+    /*@ assert 0 <= size < 65536; */
     if(size==0 ||
-	fread(dd, sizeof(struct dd_struct)*size, 1, file_recovery->handle) !=1)
+	fread(dd_buf, sizeof(struct dd_struct)*size, 1, handle) !=1)
     {
-      free(dd);
-      file_recovery->file_size=0;
-      return ;
+      return 0;
     }
 #ifdef __FRAMAC__
-    Frama_C_make_unknown(dd, sizeof(struct dd_struct)*size);
+    Frama_C_make_unknown(dd_buf, sizeof(struct dd_struct)*size);
 #endif
     if(file_size < offset + sizeof(struct dd_struct) * size)
       file_size = offset + sizeof(struct dd_struct) * size;
 #ifdef DEBUG_HDF
-    log_info("size=%u next=%lu\n", size, be32(ddh.next));
+    log_info("size=%u next=%lu\n", size, be32(ddh->next));
 #endif
     /*@
+      @ loop invariant 0 <= i <= size;
       @ loop assigns i, file_size;
       @*/
     for(i=0; i < size; i++)
@@ -123,14 +131,28 @@ static void file_check_hdf(file_recovery_t *file_recovery)
 	file_size = (uint64_t)p_offset + (uint64_t)p_length;
     }
     offset_old=offset;
-    offset=be32(ddh.next);
+    offset=be32(ddh->next);
   } while(offset > offset_old);
-  free(dd);
   file_size++;
+  return file_size;
+}
+
+/*@
+  @ requires \separated(file_recovery, file_recovery->handle, &errno, &Frama_C_entropy_source, &__fc_heap_status);
+  @ requires valid_file_check_param(file_recovery);
+  @ ensures  valid_file_check_result(file_recovery);
+  @*/
+static void file_check_hdf(file_recovery_t *file_recovery)
+{
+  uint64_t file_size;
+  char *dd;
+  dd=(char *)MALLOC(sizeof(struct dd_struct)*65536);
+  file_size = file_check_hdf_aux(file_recovery->handle, dd);
+  free(dd);
 #ifdef DEBUG_HDF
   log_info("file_size %llu\n", (long long unsigned)file_size);
 #endif
-  if(file_recovery->file_size < file_size)
+  if(file_recovery->file_size < file_size || file_size==0)
     file_recovery->file_size=0;
   else
     file_recovery->file_size = file_size;