diff --git a/src/common.c b/src/common.c
index 0adf4587..59b412f5 100644
--- a/src/common.c
+++ b/src/common.c
@@ -199,6 +199,9 @@ unsigned int up2power(const unsigned int number)
 void set_part_name(partition_t *partition, const char *src, const unsigned int max_size)
 {
   unsigned int i;
+  /*@
+    @ loop assigns i, partition->fsname[i];
+    @*/
   for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
     partition->fsname[i]=src[i];
   partition->fsname[i]='\0';
@@ -207,8 +210,14 @@ void set_part_name(partition_t *partition, const char *src, const unsigned int m
 void set_part_name_chomp(partition_t *partition, const unsigned char *src, const unsigned int max_size)
 {
   unsigned int i;
+  /*@
+    @ loop assigns i, partition->fsname[i];
+    @*/
   for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
     partition->fsname[i]=src[i];
+  /*@
+    @ loop assigns i;
+    @*/
   while(i>0 && src[i-1]==' ')
     i--;
   partition->fsname[i]='\0';
@@ -270,8 +279,6 @@ time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
   day   = td_max(1, f_date & 0x1f) - 1;
   /*@ assert 0 <= day <= 30; */
 
-  leap_day = (year + 3) / 4;
-  /*@ assert 0 <= leap_day <= 32; */
   if (year > YEAR_2100)		/* 2100 isn't leap year */
   {
     /*@ assert year > YEAR_2100; */
@@ -283,6 +290,7 @@ time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
   else
   {
     /*@ assert year <= YEAR_2100; */
+    leap_day = (year + 3) / 4;
     /*@ assert 0 <= leap_day <= (YEAR_2100 + 3)/4; */
   }
   /*@ assert 0 <= leap_day < 32; */
@@ -341,7 +349,9 @@ void set_secwest(void)
 #define NTFS_TIME_OFFSET ((int64_t)(369 * 365 + 89) * 24 * 3600 * 10000000)
 time_t td_ntfs2utc (int64_t ntfstime)
 {
-  return (ntfstime - (NTFS_TIME_OFFSET)) / 10000000;
+  if(ntfstime < NTFS_TIME_OFFSET)
+    return 0;
+  return (ntfstime - NTFS_TIME_OFFSET) / 10000000;
 }
 
 int check_command(char **current_cmd, const char *cmd, const size_t n)
@@ -349,7 +359,17 @@ int check_command(char **current_cmd, const char *cmd, const size_t n)
   const int res=strncmp(*current_cmd, cmd, n);
   if(res==0)
   {
+#ifdef __FRAMAC__
+    unsigned int i;
+    /*@
+      @ loop invariant valid_read_string(*current_cmd);
+      @ loop assigns i, *current_cmd;
+      @*/
+    for(i=0; i<n && *current_cmd!='\0'; i++)
+      (*current_cmd)++;
+#else
     (*current_cmd)+=n;
+#endif
     /*@ assert valid_read_string(*current_cmd); */
     return 0;
   }
diff --git a/src/file_asf.c b/src/file_asf.c
index 616fa825..f9291b4e 100644
--- a/src/file_asf.c
+++ b/src/file_asf.c
@@ -33,8 +33,8 @@
 #include "log.h"
 
 #if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_asf)
+/*@ requires \valid(file_stat); */
 static void register_header_check_asf(file_stat_t *file_stat);
-static int header_check_asf(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);
 
 const file_hint_t file_hint_asf= {
   .extension="asf",
@@ -58,7 +58,7 @@ struct asf_file_prop_s {
   uint64_t      object_size;
   unsigned char file_id[16];
   uint64_t      file_size;
-  uint64_t      file_date;
+  int64_t       file_date;
 } __attribute__ ((gcc_struct, __packed__));
 
 struct asf_stream_prop_s {
@@ -70,6 +70,16 @@ struct asf_stream_prop_s {
 static const char *extension_wma="wma";
 static const char *extension_wmv="wmv";
 
+/*@
+  @ requires buffer_size > sizeof(struct asf_header_obj_s);
+  @ requires \valid_read(buffer+(0..buffer_size-1));
+  @ requires valid_file_recovery(file_recovery);
+  @ requires \valid(file_recovery_new);
+  @ requires file_recovery_new->blocksize > 0;
+  @ requires separation: \separated(&file_hint_asf, buffer+(..), file_recovery, file_recovery_new);
+  @ assigns  *file_recovery_new;
+  @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @*/
 static int header_check_asf(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)
 {
   const struct asf_header_obj_s *hdr=(const struct asf_header_obj_s*)buffer;
@@ -84,6 +94,9 @@ static int header_check_asf(const unsigned char *buffer, const unsigned int buff
       le64(hdr->object_size) >= PHOTOREC_MAX_FILE_SIZE ||
       nbr_header_obj<4)
     return 0;
+  /*@
+    @ loop assigns extension, i, size, time, offset_prop;
+    @*/
   for(i=0;
       i < nbr_header_obj && offset_prop + 0x28 < buffer_size;
       i++)
@@ -102,7 +115,9 @@ static int header_check_asf(const unsigned char *buffer, const unsigned int buff
     };
     if(object_size < 0x18)
     {
+#ifndef __FRAMAC__
       log_info("header_check_asf object_size too small %llu\n", (long long unsigned)object_size);
+#endif
       return 0;
     }
     if(object_size > 0x8000000000000000)
@@ -119,10 +134,10 @@ static int header_check_asf(const unsigned char *buffer, const unsigned int buff
     else if(memcmp(prop->object_id, asf_stream_prop_s, sizeof(asf_stream_prop_s))==0)
     {
       const struct asf_stream_prop_s *stream=(const struct asf_stream_prop_s *)prop;
-      const char wma[16]={
+      const unsigned char wma[16]={
 	0x40, 0x9e, 0x69, 0xf8, 0x4d, 0x5b, 0xcf, 0x11, 0xa8, 0xfd, 0x00, 0x80, 0x5f, 0x5c, 0x44, 0x2b
       };
-      const char wmv[16]={
+      const unsigned char wmv[16]={
 	0xc0, 0xef, 0x19, 0xbc, 0x4d, 0x5b, 0xcf, 0x11, 0xa8, 0xfd, 0x00, 0x80, 0x5f, 0x5c, 0x44, 0x2b
       };
       if(object_size < 0x28)
diff --git a/src/file_reg.c b/src/file_reg.c
index 98afdf48..d672f5ce 100644
--- a/src/file_reg.c
+++ b/src/file_reg.c
@@ -32,6 +32,7 @@
 #include "common.h"
 #include "filegen.h"
 
+/*@ requires \valid(file_stat); */
 static void register_header_check_reg(file_stat_t *file_stat);
 
 const file_hint_t file_hint_reg= {
@@ -70,6 +71,16 @@ struct rgdb_block
   uint32_t chksum;
 } __attribute__ ((gcc_struct, __packed__));
 
+/*@
+  @ requires buffer_size > sizeof(struct creg_file_header);
+  @ requires \valid_read(buffer+(0..buffer_size-1));
+  @ requires valid_file_recovery(file_recovery);
+  @ requires \valid(file_recovery_new);
+  @ requires file_recovery_new->blocksize > 0;
+  @ requires separation: \separated(&file_hint_reg, buffer+(..), file_recovery, file_recovery_new);
+  @ assigns  *file_recovery_new;
+  @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @*/
 static int header_check_reg_9x(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)
 {
   const struct creg_file_header*header=(const struct creg_file_header*)buffer;
@@ -91,7 +102,7 @@ struct regf_file_header
   uint32_t signature;
   uint32_t primary_sequence_number;
   uint32_t secondary_sequence_number;
-  uint64_t modification_time;
+  int64_t  modification_time;
   uint32_t major_version;
   uint32_t minor_version;
   uint32_t file_type;
@@ -104,6 +115,16 @@ struct regf_file_header
   uint32_t xor_checksum;
 } __attribute__ ((gcc_struct, __packed__));
 
+/*@
+  @ requires buffer_size > sizeof(struct regf_file_header);
+  @ requires \valid_read(buffer+(0..buffer_size-1));
+  @ requires valid_file_recovery(file_recovery);
+  @ requires \valid(file_recovery_new);
+  @ requires file_recovery_new->blocksize > 0;
+  @ requires separation: \separated(&file_hint_reg, buffer+(..), file_recovery, file_recovery_new);
+  @ assigns  *file_recovery_new;
+  @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @*/
 static int header_check_reg_nt(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)
 {
   const struct regf_file_header *header=(const struct regf_file_header*)buffer;