diff --git a/src/fidentify.c b/src/fidentify.c
index be44e6be..149487f2 100644
--- a/src/fidentify.c
+++ b/src/fidentify.c
@@ -60,6 +60,9 @@ extern file_check_list_t file_check_list;
 #define OPT_CHECK 1
 #define OPT_TIME  2
 
+/*@
+  @ requires valid_read_string(filename);
+  @*/
 static int file_identify(const char *filename, const unsigned int options)
 {
   const unsigned int blocksize=65536;
@@ -96,6 +99,7 @@ static int file_identify(const char *filename, const unsigned int options)
 	td_list_for_each(tmp, &pos->file_checks[buffer[pos->offset]].list)
 	{
 	  const file_check_t *file_check=td_list_entry_const(tmp, const file_check_t, list);
+	  /*@ assert &file_check->header_check != \null; */
 	  if((file_check->length==0 || memcmp(buffer + file_check->offset, file_check->value, file_check->length)==0) &&
 	      file_check->header_check(buffer, blocksize, 0, &file_recovery, &file_recovery_new)!=0)
 	  {
@@ -112,13 +116,15 @@ static int file_identify(const char *filename, const unsigned int options)
 	  ((options&OPT_CHECK)!=0 || ((options&OPT_TIME)!=0 && file_recovery_new.time==0))
 	)
       {
+	off_t file_size;
 	file_recovery_new.handle=file;
 	my_fseek(file_recovery_new.handle, 0, SEEK_END);
-#ifdef HAVE_FTELLO
-	file_recovery_new.file_size=ftello(file_recovery_new.handle);
+#if defined(HAVE_FTELLO) && !defined(__FRAMAC__)
+	file_size=ftello(file_recovery_new.handle);
 #else
-	file_recovery_new.file_size=ftell(file_recovery_new.handle);
+	file_size=ftell(file_recovery_new.handle);
 #endif
+	file_recovery_new.file_size=(file_size==-1?0:file_size);
 	file_recovery_new.calculated_file_size=file_recovery_new.file_size;
 	(file_recovery_new.file_check)(&file_recovery_new);
 	if(file_recovery_new.file_size < file_recovery_new.min_filesize)
@@ -148,7 +154,7 @@ static int file_identify(const char *filename, const unsigned int options)
   return 0;
 }
 
-#ifndef __AFL_COMPILER
+#if !defined(__AFL_COMPILER) && !defined(MAIN_fidentify)
 static void file_identify_dir(const char *current_dir, const unsigned int options)
 {
   DIR *dir;
@@ -201,20 +207,27 @@ static void display_version(void)
 #ifdef RECORD_COMPILATION_DATE
   printf("Compilation date: %s\n", get_compilation_date());
 #endif
+#ifndef MAIN_fidentify
   printf("libjpeg: %s, zlib: %s\n", td_jpeg_version(), td_zlib_version());
   printf("OS: %s\n" , get_os());
+#endif
 }
 
 int main(int argc, char **argv)
 {
   int i;
+#ifdef MAIN_fidentify
+  unsigned int options=OPT_CHECK|OPT_TIME;
+#else
   unsigned int options=0;
+#endif
   FILE *log_handle=NULL;
   int log_errno=0;
   int enable_all_formats=1;
   int scan_dir=1;
   file_stat_t *file_stats;
   log_set_levels(LOG_LEVEL_DEBUG|LOG_LEVEL_TRACE|LOG_LEVEL_QUIET|LOG_LEVEL_INFO|LOG_LEVEL_VERBOSE|LOG_LEVEL_PROGRESS|LOG_LEVEL_WARNING|LOG_LEVEL_ERROR|LOG_LEVEL_PERROR|LOG_LEVEL_CRITICAL);
+#ifndef MAIN_fidentify
   for(i=1; i<argc; i++)
   {
     if( strcmp(argv[i], "/check")==0 || strcmp(argv[i], "-check")==0 || strcmp(argv[i], "--check")==0)
@@ -239,24 +252,28 @@ int main(int argc, char **argv)
       return 0;
     }
   }
+#endif
 #ifndef __AFL_COMPILER
   log_handle=log_open("fidentify.log", TD_LOG_CREATE, &log_errno);
   if(log_handle!=NULL)
   {
     time_t my_time;
-#ifdef HAVE_DUP2
+#if defined(HAVE_DUP2) && !defined(__FRAMAC__)
     dup2(fileno(log_handle),2);
 #endif
     my_time=time(NULL);
     log_info("\n\n%s",ctime(&my_time));
     log_info("Command line: fidentify");
+#ifndef MAIN_fidentify
     for(i=1;i<argc;i++)
       log_info(" %s", argv[i]);
+#endif
     log_info("\n\n");
     log_flush();
   }
   log_info("fidentify %s, Data Recovery Utility, %s\nChristophe GRENIER <grenier@cgsecurity.org>\nhttps://www.cgsecurity.org\n", VERSION, TESTDISKDATE);
 #endif
+#ifndef MAIN_fidentify
   for(i=1; i<argc; i++)
   {
     file_enable_t *file_enable;
@@ -269,6 +286,7 @@ int main(int argc, char **argv)
 	enable_all_formats=0;
       }
   }
+#endif
   if(enable_all_formats)
   {
     /* Enable all file formats */
@@ -277,6 +295,7 @@ int main(int argc, char **argv)
       file_enable->enable=1;
   }
   file_stats=init_file_stats(list_file_enable);
+#ifndef MAIN_fidentify
   for(i=1; i<argc; i++)
   {
     if(strcmp(argv[i], "/check")==0 || strcmp(argv[i], "-check")==0 || strcmp(argv[i], "--check")==0 ||
@@ -306,6 +325,9 @@ int main(int argc, char **argv)
 #ifndef __AFL_COMPILER
   if(scan_dir)
     file_identify_dir(".", options);
+#endif
+#else
+  file_identify("demo", options);
 #endif
   free_header_check();
   free(file_stats);
diff --git a/src/file_bmp.c b/src/file_bmp.c
index 090f538e..afef52bb 100644
--- a/src/file_bmp.c
+++ b/src/file_bmp.c
@@ -130,6 +130,8 @@ static int header_check_bmp(const unsigned char *buffer, const unsigned int buff
     /*@ assert file_recovery_new->min_filesize == 65; */
     /*@ assert file_recovery_new->data_check == &data_check_size; */
     /*@ assert file_recovery_new->file_check == &file_check_size; */
+    /*@ assert valid_read_string(file_recovery_new->extension); */
+    /*@ assert \initialized(&file_recovery_new->time); */
     return 1;
   }
   return 0;
@@ -145,7 +147,7 @@ static void register_header_check_bmp(file_stat_t *file_stat)
 
 #if defined(MAIN_bmp)
 #define BLOCKSIZE 65536u
-int main()
+int main(void)
 {
   const char fn[] = "recup_dir.1/f0000000.bmp";
   unsigned char buffer[BLOCKSIZE];
diff --git a/src/file_list.c b/src/file_list.c
index 5e8867ee..0c6b1835 100644
--- a/src/file_list.c
+++ b/src/file_list.c
@@ -366,6 +366,7 @@ extern const file_hint_t file_hint_zpr;
 
 file_enable_t list_file_enable[]=
 {
+#ifndef MAIN_fidentify
   { .enable=0, .file_hint=&file_hint_sig  },
   { .enable=0, .file_hint=&file_hint_1cd  },
   { .enable=0, .file_hint=&file_hint_3dm  },
@@ -405,7 +406,9 @@ file_enable_t list_file_enable[]=
   { .enable=0, .file_hint=&file_hint_binvox  },
   { .enable=0, .file_hint=&file_hint_bkf  },
   { .enable=0, .file_hint=&file_hint_blend },
+#endif
   { .enable=0, .file_hint=&file_hint_bmp  },
+#ifndef MAIN_fidentify
   { .enable=0, .file_hint=&file_hint_bpg  },
   { .enable=0, .file_hint=&file_hint_bvr  },
   { .enable=0, .file_hint=&file_hint_bz2  },
@@ -702,6 +705,7 @@ file_enable_t list_file_enable[]=
   { .enable=0, .file_hint=&file_hint_zcode  },
   { .enable=0, .file_hint=&file_hint_zip  },
   { .enable=0, .file_hint=&file_hint_zpr  },
+#endif
   { .enable=0, .file_hint=NULL }
 };
 
diff --git a/src/filegen.c b/src/filegen.c
index e76010c1..70b69136 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -182,6 +182,11 @@ void free_header_check(void)
   {
     unsigned int i;
     file_check_list_t *pos=td_list_entry(tmpl, file_check_list_t, list);
+    /*@
+      @ loop unroll 256;
+      @ loop invariant 0 <= i <= 256;
+      @*/
+    /* TODO loop variant 255-i; */
     for(i=0;i<256;i++)
     {
       struct td_list_head *tmp;
diff --git a/src/list.h b/src/list.h
index 265e7fe3..c4fbe67c 100644
--- a/src/list.h
+++ b/src/list.h
@@ -124,10 +124,19 @@ static inline void td_list_add_tail(struct td_list_head *newe, struct td_list_he
  * This is only for internal list manipulation where we know
  * the prev/next entries already!
  */
+/*@
+  @ requires \valid(prev);
+  @ requires \valid(next);
+  @ ensures next->prev == prev;
+  @ ensures prev->next == next;
+  @ assigns next->prev,prev->next;
+  @*/
 static inline void __td_list_del(struct td_list_head * prev, struct td_list_head * next)
 {
 	next->prev = prev;
 	prev->next = next;
+	/*@ assert next->prev == prev; */
+	/*@ assert prev->next == next; */
 }
 
 /**
@@ -136,11 +145,23 @@ static inline void __td_list_del(struct td_list_head * prev, struct td_list_head
  * Note: td_list_empty on entry does not return true after this, the entry is
  * in an undefined state.
  */
+/*@
+  @ requires \valid(entry);
+  @ requires \valid(entry->prev);
+  @ requires \valid(entry->next);
+  @ ensures \old(entry->prev)->next == \old(entry->next);
+  @ ensures \old(entry->next)->prev == \old(entry->prev);
+  @ assigns \old(entry->prev)->next, \old(entry->next)->prev, entry->next, entry->prev;
+  @*/
 static inline void td_list_del(struct td_list_head *entry)
 {
 	__td_list_del(entry->prev, entry->next);
+	/*@ assert entry->prev->next == entry->next; */
+	/*@ assert entry->next->prev == entry->prev; */
 	entry->next = (struct td_list_head*)LIST_POISON1;
 	entry->prev = (struct td_list_head*)LIST_POISON2;
+	/*@ assert \at(entry->prev,Pre)->next == \at(entry->next,Pre); */
+	/*@ assert \at(entry->next,Pre)->prev == \at(entry->prev,Pre); */
 }
 
 /**
diff --git a/src/misc.c b/src/misc.c
index 8ac00d66..fb89ce81 100644
--- a/src/misc.c
+++ b/src/misc.c
@@ -172,7 +172,7 @@ https://msdn.microsoft.com/en-us/library/windows/desktop/ms724834%28v=vs.85%29.a
   }
 #elif defined(DJGPP)
   return "DOS";
-#elif defined(HAVE_SYS_UTSNAME_H) && defined(HAVE_UNAME)
+#elif defined(HAVE_SYS_UTSNAME_H) && defined(HAVE_UNAME) && !defined(__FRAMAC__)
   {
     struct utsname Ver;
     if(uname(&Ver)==0)
@@ -281,7 +281,7 @@ const char *get_compilation_date(void)
 {
   static char buffer[100] = {0x00};
 #ifdef __DATE__ 
-#ifdef HAVE_STRPTIME
+#if defined(HAVE_STRPTIME) && !defined(__FRAMAC__)
   struct tm tm;
   memset(&tm,0,sizeof(tm));
   if(strptime(__DATE__, "%b %d %Y", &tm)!=NULL)