diff --git a/src/common.c b/src/common.c
index afcf3871..8e9e7de2 100644
--- a/src/common.c
+++ b/src/common.c
@@ -225,22 +225,50 @@ char* strip_dup(char* str)
 }
 
 /* Convert a MS-DOS time/date pair to a UNIX date (seconds since 1 1 70). */
+/*
+ * The epoch of FAT timestamp is 1980.
+ *     :  bits :     value
+ * date:  0 -  4: day	(1 -  31)
+ * date:  5 -  8: month	(1 -  12)
+ * date:  9 - 15: year	(0 - 127) from 1980
+ * time:  0 -  4: sec	(0 -  29) 2sec counts
+ * time:  5 - 10: min	(0 -  59)
+ * time: 11 - 15: hour	(0 -  23)
+ */
+#define SECS_PER_MIN	60
+#define SECS_PER_HOUR	(60 * 60)
+#define SECS_PER_DAY	(SECS_PER_HOUR * 24)
+/* days between 1.1.70 and 1.1.80 (2 leap days) */
+#define DAYS_DELTA	(365 * 10 + 2)
+/* 120 (2100 - 1980) isn't leap year */
+#define YEAR_2100	120
+#define IS_LEAP_YEAR(y)	(!((y) & 3) && (y) != YEAR_2100)
 
 time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
 {
-  static const unsigned int day_n[] = { 0,31,59,90,120,151,181,212,243,273,304,334,0,0,0,0 };
+  static const unsigned int days_in_year[] = { 0, 0,31,59,90,120,151,181,212,243,273,304,334,0,0,0 };
   /* JanFebMarApr May Jun Jul Aug Sep Oct Nov Dec */
 
-  unsigned int month,year,secs;
+  unsigned long int day,leap_day,month,year,days;
+  unsigned long int secs;
+  year  = f_date >> 9;
+  month = td_max(1, (f_date >> 5) & 0xf);
+  day   = td_max(1, f_date & 0x1f) - 1;
+
+  leap_day = (year + 3) / 4;
+  if (year > YEAR_2100)		/* 2100 isn't leap year */
+    leap_day--;
+  if (IS_LEAP_YEAR(year) && month > 2)
+    leap_day++;
+  days = days_in_year[month];
+  /*@ assert days <= 334; */
+  days += year * 365 + leap_day + day + DAYS_DELTA;
+
+  secs = (f_time & 0x1f)<<1;
+  secs += ((f_time >> 5) & 0x3f) * SECS_PER_MIN;
+  secs += (f_time >> 11)* SECS_PER_HOUR;
+  secs += days * SECS_PER_DAY;
 
-  /* first subtract and mask after that... Otherwise, if
-     f_date == 0, bad things happen */
-  month = ((f_date >> 5) - 1) & 15;
-  year = f_date >> 9;
-  secs = (f_time & 31)*2+60*((f_time >> 5) & 63)+(f_time >> 11)*3600+86400*
-    ((f_date & 31)-1+day_n[month]+(year/4)+year*365-((year & 3) == 0 &&
-      month < 2 ? 1 : 0)+3653);
-  /* days since 1.1.70 plus 80's leap day */
   return secs+secwest;
 }
 
diff --git a/src/common.h b/src/common.h
index 8a5e5ea9..a7361fd3 100644
--- a/src/common.h
+++ b/src/common.h
@@ -449,6 +449,8 @@ unsigned int up2power(const unsigned int number);
 void set_part_name(partition_t *partition, const char *src, const unsigned int max_size);
 void set_part_name_chomp(partition_t *partition, const unsigned char *src, const unsigned int max_size);
 char* strip_dup(char* str);
+
+/*@ assigns \nothing; */
 time_t date_dos2unix(const unsigned short f_time,const unsigned short f_date);
 void set_secwest(void);
 time_t td_ntfs2utc (int64_t ntfstime);
diff --git a/src/fidentify.c b/src/fidentify.c
index 24b95442..be44e6be 100644
--- a/src/fidentify.c
+++ b/src/fidentify.c
@@ -85,9 +85,10 @@ static int file_identify(const char *filename, const unsigned int options)
       file_recovery_t file_recovery_new;
       file_recovery_t file_recovery;
       reset_file_recovery(&file_recovery);
+      reset_file_recovery(&file_recovery_new);
       file_recovery.blocksize=blocksize;
       file_recovery_new.blocksize=blocksize;
-      file_recovery_new.file_stat=NULL;
+      /*@ assert file_recovery_new.file_stat==NULL; */
       td_list_for_each(tmpl, &file_check_list.list)
       {
 	struct td_list_head *tmp;
diff --git a/src/filegen.c b/src/filegen.c
index 1ad22705..93912c17 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -235,14 +235,23 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
   {
     int i;
     int taille;
-    const unsigned int read_size=(offset%4096!=0 ? offset%4096 : 4096);
-    offset-=read_size;
+    if(offset <= 4096)
+      offset=0;
+    else if(offset%4096==0)
+      offset-=4096;
+    else
+      offset=offset-(offset%4096);
     if(my_fseek(handle,offset,SEEK_SET)<0)
     {
       free(buffer);
       return 0;
     }
-    taille=fread(buffer, 1, read_size, handle);
+    taille=fread(buffer, 1, 4096, handle);
+    if(taille <= 0)
+    {
+      free(buffer);
+      return 0;
+    }
     for(i=taille-1;i>=0;i--)
     {
       if(buffer[i]==*(const unsigned char *)footer && memcmp(buffer+i,footer,footer_length)==0)
@@ -264,6 +273,7 @@ void file_search_footer(file_recovery_t *file_recovery, const void*footer, const
   file_recovery->file_size=file_rsearch(file_recovery->handle, file_recovery->file_size-extra_length, footer, footer_length);
   if(file_recovery->file_size > 0)
     file_recovery->file_size+= footer_length + extra_length;
+  /*@ assert \valid(file_recovery->handle); */
 }
 
 #if 0
@@ -577,13 +587,6 @@ static int _file_rename(file_recovery_t *file_recovery, const void *buffer, cons
   return -1;
 }
 
-/*@
-  @ requires \valid(file_recovery);
-  @ requires valid_read_string((char*)&file_recovery->filename);
-  @ requires \valid_read((char *)buffer+(0..buffer_size-1));
-  @ requires new_ext==\null || valid_read_string(new_ext);
-  @ ensures valid_read_string((char*)&file_recovery->filename);
-  @*/
 /* The original filename begins at offset in buffer and is null terminated */
 int file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
 {
@@ -707,13 +710,6 @@ static int _file_rename_unicode(file_recovery_t *file_recovery, const void *buff
   return -1;
 }
 
-/*@
-  @ requires \valid(file_recovery);
-  @ requires valid_read_string((char*)&file_recovery->filename);
-  @ requires \valid_read((char *)buffer+(0..buffer_size-1));
-  @ requires new_ext==\null || valid_read_string(new_ext);
-  @ ensures valid_read_string((char*)&file_recovery->filename);
-  @*/
 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 append_original_ext)
 {
   if(buffer!=NULL && 0 <= offset && offset < buffer_size &&
diff --git a/src/filegen.h b/src/filegen.h
index a79d07a9..7a1807b3 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -123,6 +123,7 @@ void free_header_check(void);
 /*@
   @ requires \valid(file_recovery);
   @ requires \valid(file_recovery->handle);
+  @ ensures \valid(file_recovery->handle);
   @*/
 void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode);
 
@@ -135,8 +136,10 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
 
 /*@
   @ requires \valid(file_recovery);
+  @ requires \valid(file_recovery->handle);
   @ requires footer_length > 0;
   @ requires \valid_read((char *)footer+(0..footer_length-1));
+  @ ensures \valid(file_recovery->handle);
   @*/
 void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length);
 
@@ -153,18 +156,21 @@ data_check_t data_check_size(const unsigned char *buffer, const unsigned int buf
 /*@
   @ requires \valid(file_recovery);
   @ requires file_recovery->file_check == &file_check_size;
+  @ assigns file_recovery->file_size;
   @*/
 void file_check_size(file_recovery_t *file_recovery);
 
 /*@
   @ requires \valid(file_recovery);
   @ requires file_recovery->file_check == &file_check_size_min;
+  @ assigns file_recovery->file_size;
   @*/
 void file_check_size_min(file_recovery_t *file_recovery);
 
 /*@
   @ requires \valid(file_recovery);
   @ requires file_recovery->file_check == &file_check_size_max;
+  @ assigns file_recovery->file_size;
   @*/
 void file_check_size_max(file_recovery_t *file_recovery);
 
@@ -236,6 +242,7 @@ file_stat_t * init_file_stats(file_enable_t *files_enable);
   @ requires valid_read_string((char*)&file_recovery->filename);
   @ requires \valid_read((char *)buffer+(0..buffer_size-1));
   @ requires new_ext==\null || valid_read_string(new_ext);
+  @ ensures valid_read_string((char*)&file_recovery->filename);
   @*/
 int file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int force_ext);
 
@@ -244,6 +251,7 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
   @ requires valid_read_string((char*)&file_recovery->filename);
   @ requires \valid_read((char *)buffer+(0..buffer_size-1));
   @ requires new_ext==\null || valid_read_string(new_ext);
+  @ ensures valid_read_string((char*)&file_recovery->filename);
   @*/
 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);