diff --git a/src/file_tiff.c b/src/file_tiff.c
index 17edb1f9..a5f00cfc 100644
--- a/src/file_tiff.c
+++ b/src/file_tiff.c
@@ -43,7 +43,7 @@
 #include "__fc_builtin.h"
 #endif
 
-/*@ requires \valid(file_stat); */
+/*@ requires valid_register_header_check(file_stat); */
 static void register_header_check_tiff(file_stat_t *file_stat);
 
 const file_hint_t file_hint_tiff= {
diff --git a/src/file_tiff.h b/src/file_tiff.h
index d74e721f..12df8161 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -98,15 +98,9 @@ unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const uns
 
 #if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg)
 /*@
-  @ requires \valid(fr);
-  @ requires \valid(fr->handle);
-  @ requires valid_file_recovery(fr);
-  @ requires \valid_read(&fr->extension);
-  @ requires valid_read_string(fr->extension);
   @ requires fr->file_check==&file_check_tiff_le;
-  @ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
-  @ ensures \valid(fr->handle);
-  @ ensures valid_read_string(fr->extension);
+  @ requires valid_file_check_param(fr);
+  @ ensures  valid_file_check_result(fr);
   @ assigns  errno;
   @ assigns  fr->file_size;
   @ assigns  *fr->handle;
@@ -117,31 +111,16 @@ void file_check_tiff_le(file_recovery_t *fr);
 
 #if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf) && !defined(SINGLE_FORMAT_wdp)
 /*@
-  @ requires buffer_size > 0;
-  @ 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;
-  @
   @ requires buffer_size >= 15;
-  @
-  @ 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) ==> \initialized(&file_recovery_new->calculated_file_size);
+  @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
-  @ ensures (\result == 1) ==> \initialized(&file_recovery_new->min_filesize);
   @ 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);
-  @
   @ ensures (\result == 1) ==> (file_recovery_new->calculated_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!=0 ==> valid_file_recovery(file_recovery_new);
   @*/
 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
@@ -160,30 +139,15 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsi
 
 #if !defined(MAIN_tiff_le) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf) && !defined(SINGLE_FORMAT_wdp)
 /*@
-  @ requires buffer_size > 0;
-  @ 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;
-  @
   @ requires buffer_size >= 15;
-  @
-  @ 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) ==> \initialized(&file_recovery_new->calculated_file_size);
+  @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
-  @ ensures (\result == 1) ==> \initialized(&file_recovery_new->min_filesize);
   @ 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);
-  @
   @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
   @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
   @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
-  @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
   @*/
 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 b667b64a..3a3d9905 100644
--- a/src/file_tiff_be.c
+++ b/src/file_tiff_be.c
@@ -712,15 +712,9 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
 }
 
 /*@
-  @ requires \valid(fr);
-  @ requires \valid(fr->handle);
-  @ requires valid_file_recovery(fr);
-  @ requires \valid_read(&fr->extension);
-  @ requires valid_read_string(fr->extension);
   @ requires fr->file_check==&file_check_tiff_be;
-  @ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
-  @ ensures \valid(fr->handle);
-  @ ensures valid_read_string(fr->extension);
+  @ requires valid_file_check_param(fr);
+  @ ensures  valid_file_check_result(fr);
   @ assigns  errno;
   @ assigns  fr->file_size;
   @ assigns  *fr->handle;
@@ -729,19 +723,20 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
 static void file_check_tiff_be(file_recovery_t *fr)
 {
   static uint64_t calculated_file_size=0;
-  TIFFHeader header;
+  char buffer[sizeof(TIFFHeader)];
+  const TIFFHeader *header=(const TIFFHeader *)&buffer;
   calculated_file_size = 0;
   if(fseek(fr->handle, 0, SEEK_SET) < 0 ||
-      fread(&header, sizeof(TIFFHeader), 1, fr->handle) != 1)
+      fread(&buffer, sizeof(TIFFHeader), 1, fr->handle) != 1)
   {
     fr->file_size=0;
     return;
   }
 #if defined(__FRAMAC__)
-  Frama_C_make_unknown((char *)&header, sizeof(TIFFHeader));
+  Frama_C_make_unknown(&buffer, sizeof(TIFFHeader));
 #endif
-  if(header.tiff_magic==TIFF_BIGENDIAN)
-    calculated_file_size=file_check_tiff_be_aux(fr, be32(header.tiff_diroff), 0, 0);
+  if(header->tiff_magic==TIFF_BIGENDIAN)
+    calculated_file_size=file_check_tiff_be_aux(fr, be32(header->tiff_diroff), 0, 0);
   /*@ assert \valid(fr->handle); */
 #ifdef DEBUG_TIFF
   log_info("TIFF Current   %llu\n", (unsigned long long)fr->file_size);
diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c
index f12d98ee..f597d46d 100644
--- a/src/file_tiff_le.c
+++ b/src/file_tiff_le.c
@@ -726,19 +726,20 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
 void file_check_tiff_le(file_recovery_t *fr)
 {
   static uint64_t calculated_file_size=0;
-  TIFFHeader header;
+  char buffer[sizeof(TIFFHeader)];
+  const TIFFHeader *header=(const TIFFHeader *)&buffer;
   calculated_file_size = 0;
   if(fseek(fr->handle, 0, SEEK_SET) < 0 ||
-      fread(&header, sizeof(TIFFHeader), 1, fr->handle) != 1)
+      fread(&buffer, sizeof(TIFFHeader), 1, fr->handle) != 1)
   {
     fr->file_size=0;
     return;
   }
 #if defined(__FRAMAC__)
-  Frama_C_make_unknown((char *)&header, sizeof(TIFFHeader));
+  Frama_C_make_unknown(&buffer, sizeof(TIFFHeader));
 #endif
-  if(header.tiff_magic==TIFF_LITTLEENDIAN)
-    calculated_file_size=file_check_tiff_le_aux(fr, le32(header.tiff_diroff), 0, 0);
+  if(header->tiff_magic==TIFF_LITTLEENDIAN)
+    calculated_file_size=file_check_tiff_le_aux(fr, le32(header->tiff_diroff), 0, 0);
   /*@ assert \valid(fr->handle); */
 #ifdef DEBUG_TIFF
   log_info("TIFF Current   %llu\n", (unsigned long long)fr->file_size);