diff --git a/src/file_tiff.h b/src/file_tiff.h
index 51059f51..fa9af035 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -77,7 +77,7 @@ time_t get_date_from_tiff_header(const unsigned char*buffer, const unsigned int
 /*@
   @ requires \valid_read(buffer+(0..buffer_size-1));
   @ requires \separated(potential_error, buffer);
-  @ ensures \valid_read(buffer+(0..buffer_size-1));
+  @ assigns *potential_error;
   @*/
 unsigned int find_tag_from_tiff_header(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int tag, const unsigned char **potential_error);
 
@@ -88,7 +88,7 @@ unsigned int find_tag_from_tiff_header(const unsigned char *buffer, const unsign
   @ requires \valid_read(buffer+(0..tiff_size-1));
   @ requires \valid(potential_error);
   @ requires \separated(potential_error, buffer);
-  @ ensures \valid_read(buffer+(0..tiff_size-1));
+  @ assigns *potential_error;
   @*/
 unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error);
 #endif
@@ -109,12 +109,21 @@ void file_check_tiff_le(file_recovery_t *fr);
   @ requires buffer_size >= 15;
   @ requires \valid_read(buffer+(0..buffer_size-1));
   @ requires \valid_read(file_recovery);
+  @ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
   @ requires \valid(file_recovery_new);
   @ requires file_recovery_new->blocksize > 0;
   @ ensures \result == 0 || \result == 1;
+  @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+  @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
+  @ ensures \result == 1 ==> \initialized(&file_recovery_new->time);
+  @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+  @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+  @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
   @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_tiff_le);
+  @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
   @ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
   @ ensures (\result == 1) ==>  valid_read_string(file_recovery_new->extension);
+  @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
   @*/
 int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new);
 #endif
@@ -126,7 +135,7 @@ int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_
   @ requires \valid_read(buffer+(0..tiff_size-1));
   @ requires \valid(potential_error);
   @ requires \separated(potential_error, buffer);
-  @ ensures \valid_read(buffer+(0..tiff_size-1));
+  @ assigns *potential_error;
   @*/
 unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error);
 #endif
@@ -136,11 +145,20 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsi
   @ requires buffer_size >= 15;
   @ requires \valid_read(buffer+(0..buffer_size-1));
   @ requires \valid_read(file_recovery);
+  @ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
   @ requires \valid(file_recovery_new);
   @ requires file_recovery_new->blocksize > 0;
   @ ensures \result == 0 || \result == 1;
+  @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+  @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
+  @ ensures \result == 1 ==> \initialized(&file_recovery_new->time);
+  @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+  @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+  @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
+  @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
   @ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
   @ ensures (\result == 1) ==>  valid_read_string(file_recovery_new->extension);
+  @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
   @*/
 int header_check_tiff_be(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new);
 #endif
diff --git a/src/file_tiff_be.c b/src/file_tiff_be.c
index dfe17a3c..84b33af8 100644
--- a/src/file_tiff_be.c
+++ b/src/file_tiff_be.c
@@ -52,10 +52,33 @@ static const char *extension_nef="nef";
 static const char *extension_pef="pef";
 
 #ifndef MAIN_tiff_le
+/*@
+  @ requires \valid_read(buffer+(0..tiff_size-1));
+  @ ensures \result <= 0xffff;
+  @ assigns \nothing;
+  @ */
+static unsigned int get_nbr_fields_be(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int offset_hdr)
+{
+  const unsigned char *ptr_hdr;
+  const struct ifd_header *hdr;
+  if(sizeof(struct ifd_header) > tiff_size)
+    return 0;
+  /*@ assert tiff_size >= sizeof(struct ifd_header); */
+  if(offset_hdr > tiff_size - sizeof(struct ifd_header))
+    return 0;
+  /*@ assert offset_hdr + sizeof(struct ifd_header) <= tiff_size; */
+  ptr_hdr=&buffer[offset_hdr];
+  /*@ assert \valid_read(ptr_hdr + (0 .. sizeof(struct ifd_header)-1)); */
+  hdr=(const struct ifd_header *)ptr_hdr;
+  /*@ assert \valid_read(hdr); */
+  return be16(hdr->nbr_fields);
+}
+
 /*@
   @ requires \valid_read(buffer+(0..tiff_size-1));
   @ requires \valid(potential_error);
   @ requires \separated(potential_error, buffer+(..));
+  @ assigns *potential_error;
   @
  */
 static unsigned int find_tag_from_tiff_header_be_aux(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error, const unsigned int offset_hdr)
@@ -143,6 +166,25 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char *buffer, const uns
     if(tmp)
       return tmp;
   }
+  {
+    const unsigned int nbr_fields=get_nbr_fields_be(buffer, tiff_size, offset_ifd0);
+    unsigned int offset_tiff_next_diroff;
+    offset_tiff_next_diroff=offset_ifd0 + 2 + nbr_fields * sizeof(TIFFDirEntry);
+    /*@ assert tiff_size >= 4; */
+    if(offset_tiff_next_diroff < tiff_size - 4)
+    {
+      const unsigned char *ptr_hdr;
+      /*@ assert offset_tiff_next_diroff + 4 <= tiff_size; */
+      ptr_hdr=&buffer[offset_tiff_next_diroff];
+      /*@ assert \valid_read(ptr_hdr + (0 .. 4-1)); */
+      const uint32_t *tiff_next_diroff=(const uint32_t *)ptr_hdr;
+      /*@ assert \valid_read(tiff_next_diroff); */
+      /* IFD1 */
+      const unsigned int offset_ifd1=be32(*tiff_next_diroff);
+      if(offset_ifd1 > 0)
+	return find_tag_from_tiff_header_be_aux(buffer, tiff_size, tag, potential_error, offset_ifd1);
+    }
+  }
   /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
   return 0;
 }
diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c
index 590e7bf9..d12f146b 100644
--- a/src/file_tiff_le.c
+++ b/src/file_tiff_le.c
@@ -56,10 +56,33 @@ static const char *extension_nef="nef";
 static const char *extension_sr2="sr2";
 
 #ifndef MAIN_tiff_be
+/*@
+  @ requires \valid_read(buffer+(0..tiff_size-1));
+  @ ensures \result <= 0xffff;
+  @ assigns \nothing;
+  @ */
+static unsigned int get_nbr_fields_le(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int offset_hdr)
+{
+  const unsigned char *ptr_hdr;
+  const struct ifd_header *hdr;
+  if(sizeof(struct ifd_header) > tiff_size)
+    return 0;
+  /*@ assert tiff_size >= sizeof(struct ifd_header); */
+  if(offset_hdr > tiff_size - sizeof(struct ifd_header))
+    return 0;
+  /*@ assert offset_hdr + sizeof(struct ifd_header) <= tiff_size; */
+  ptr_hdr=&buffer[offset_hdr];
+  /*@ assert \valid_read(ptr_hdr + (0 .. sizeof(struct ifd_header)-1)); */
+  hdr=(const struct ifd_header *)ptr_hdr;
+  /*@ assert \valid_read(hdr); */
+  return le16(hdr->nbr_fields);
+}
+
 /*@
   @ requires \valid_read(buffer+(0..tiff_size-1));
   @ requires \valid(potential_error);
   @ requires \separated(potential_error, buffer+(..));
+  @ assigns *potential_error;
   @
  */
 static unsigned int find_tag_from_tiff_header_le_aux(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error, const unsigned int offset_hdr)
@@ -146,6 +169,24 @@ unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const uns
     if(tmp)
       return tmp;
   }
+  {
+    const unsigned int nbr_fields=get_nbr_fields_le(buffer, tiff_size, offset_ifd0);
+    unsigned int offset_tiff_next_diroff;
+    offset_tiff_next_diroff=offset_ifd0 + 2 + nbr_fields * sizeof(TIFFDirEntry);
+    if(offset_tiff_next_diroff < tiff_size - 4)
+    {
+      const unsigned char *ptr_hdr;
+      /*@ assert offset_tiff_next_diroff + 4 <= tiff_size; */
+      ptr_hdr=&buffer[offset_tiff_next_diroff];
+      /*@ assert \valid_read(ptr_hdr + (0 .. 4-1)); */
+      const uint32_t *tiff_next_diroff=(const uint32_t *)ptr_hdr;
+      /*@ assert \valid_read(tiff_next_diroff); */
+      /* IFD1 */
+      const unsigned int offset_ifd1=le32(*tiff_next_diroff);
+      if(offset_ifd1 > 0)
+	return find_tag_from_tiff_header_le_aux(buffer, tiff_size, tag, potential_error, offset_ifd1);
+    }
+  }
   /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
   return 0;
 }