diff --git a/src/file_bmp.c b/src/file_bmp.c
index 841ed92a..9d8b1df8 100644
--- a/src/file_bmp.c
+++ b/src/file_bmp.c
@@ -35,6 +35,9 @@
 #include "__fc_builtin.h"
 #endif
 
+/*@
+  @ requires valid_register_header_check(file_stat);
+  @*/
 static void register_header_check_bmp(file_stat_t *file_stat);
 
 const file_hint_t file_hint_bmp= {
@@ -59,12 +62,19 @@ struct bmp_header
 
 /*@
   @ requires buffer_size >= 18;
-  @ 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 separation: \separated(&file_hint_bmp, buffer+(..), file_recovery, file_recovery_new);
+  @ 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_stat == \null);
+  @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
+  @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
+  @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_bmp.extension);
+  @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 65);
+  @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+  @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 65);
+  @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
+  @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+  @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
   @ assigns file_recovery_new->filename[0];
   @ assigns file_recovery_new->time;
   @ assigns file_recovery_new->file_stat;
@@ -86,19 +96,7 @@ struct bmp_header
   @ assigns file_recovery_new->checkpoint_offset;
   @ assigns file_recovery_new->flags;
   @ assigns file_recovery_new->extra;
-  @ 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->time == 0);
-  @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_bmp.extension);
-  @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 65);
-  @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
-  @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 65);
-  @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
-  @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
-  @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
-  @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+  @ assigns file_recovery_new->data_check_tmp;
   @*/
 // ensures (\result == 1) ==>  \separated(file_recovery_new, file_recovery_new->extension);
 static int header_check_bmp(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)
@@ -136,9 +134,6 @@ static int header_check_bmp(const unsigned char *buffer, const unsigned int buff
   return 0;
 }
 
-/*@
-  @ requires \valid(file_stat);
-  @*/
 static void register_header_check_bmp(file_stat_t *file_stat)
 {
   register_header_check(0, bmp_header,sizeof(bmp_header), &header_check_bmp, file_stat);
diff --git a/src/filegen.c b/src/filegen.c
index 975751ee..aacac1c0 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -113,6 +113,8 @@ static void file_check_add_tail(file_check_t *file_check_new, file_check_list_t
   /*@
     @ loop unroll 256;
     @ loop invariant 0 <= i <= 256;
+    @ loop invariant \forall integer j; (0 <= j < i) ==> newe->file_checks[j].list.prev == &newe->file_checks[j].list;
+    @ loop invariant \forall integer j; (0 <= j < i) ==> newe->file_checks[j].list.next == &newe->file_checks[j].list;
     @ loop assigns i, newe->file_checks[0 .. i-1].list.prev, newe->file_checks[0 .. i-1].list.next;
     @ loop variant 255-i;
     @*/
@@ -398,6 +400,7 @@ void reset_file_recovery(file_recovery_t *file_recovery)
   file_recovery->checkpoint_offset=0;
   file_recovery->flags=0;
   file_recovery->extra=0;
+  file_recovery->data_check_tmp=0;
 }
 
 file_stat_t * init_file_stats(file_enable_t *files_enable)
diff --git a/src/filegen.h b/src/filegen.h
index f20b60d3..6fe571aa 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -101,6 +101,7 @@ struct file_recovery_struct
   int checkpoint_status;	/* 0=suspend at offset_checkpoint if offset_checkpoint>0, 1=resume at offset_checkpoint */
   unsigned int blocksize;
   unsigned int flags;
+  unsigned int data_check_tmp;
 };
 
 typedef struct
@@ -300,6 +301,7 @@ void file_check_size_max(file_recovery_t *file_recovery);
   ensures file_recovery->checkpoint_offset==0;
   ensures file_recovery->flags==0;
   ensures file_recovery->extra==0;
+  ensures file_recovery->data_check_tmp==0;
   assigns file_recovery->filename[0];
   assigns file_recovery->time;
   assigns file_recovery->file_stat;
@@ -321,6 +323,7 @@ void file_check_size_max(file_recovery_t *file_recovery);
   assigns file_recovery->checkpoint_offset;
   assigns file_recovery->flags;
   assigns file_recovery->extra;
+  assigns file_recovery->data_check_tmp;
 */
 //  ensures valid_file_recovery(file_recovery);
 void reset_file_recovery(file_recovery_t *file_recovery);