diff --git a/src/Makefile.am b/src/Makefile.am
index d7494e2b..c2049ed8 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -39,7 +39,7 @@ EXTRA_PROGRAMS		= photorecf fuzzerfidentify
 smallbase_C		= common.c crc.c apfs_common.c ext2_common.c fat_common.c log.c misc.c setdate.c
 smallbase_H		= common.h crc.h apfs_common.h ext2_common.h fat_common.h log.h misc.h setdate.h
 base_C			= $(smallbase_C) autoset.c ewf.c fnctdsk.c hdaccess.c hdcache.c hdwin32.c hidden.c hpa_dco.c intrf.c iso.c list_sort.c log_part.c msdos.c parti386.c partgpt.c parthumax.c partmac.c partsun.c partnone.c partxbox.c io_redir.c ntfs_io.c ntfs_utl.c partauto.c sudo.c unicode.c win32.c
-base_H			= $(smallbase_H) alignio.h autoset.h ewf.h fnctdsk.h hdaccess.h hdwin32.h hidden.h guid_cmp.h guid_cpy.h hdcache.h hpa_dco.h intrf.h iso.h iso9660.h lang.h list.h list_sort.h log_part.h types.h io_redir.h msdos.h ntfs_utl.h parti386.h partgpt.h parthumax.h partmac.h partsun.h partxbox.h partauto.h sudo.h unicode.h win32.h
+base_H			= $(smallbase_H) apfs_common.h alignio.h autoset.h ewf.h fnctdsk.h hdaccess.h hdwin32.h hidden.h guid_cmp.h guid_cpy.h hdcache.h hpa_dco.h intrf.h iso.h iso9660.h lang.h list.h list_add_sorted.h list_add_sorted_uniq.h list_sort.h log_part.h types.h io_redir.h msdos.h ntfs_utl.h parti386.h partgpt.h parthumax.h partmac.h partsun.h partxbox.h partauto.h sudo.h unicode.h win32.h
 
 fs_C			= analyse.c apfs.c bfs.c bsd.c btrfs.c cramfs.c exfat.c ext2.c fat.c fatx.c f2fs.c jfs.c gfs2.c hfs.c hfsp.c hpfs.c luks.c lvm.c md.c netware.c ntfs.c refs.c rfs.c savehdr.c sun.c swap.c sysv.c ufs.c vmfs.c wbfs.c xfs.c zfs.c
 fs_H			= analyse.h apfs.h bfs.h bsd.h btrfs.h cramfs.h exfat.h ext2.h fat.h fatx.h f2fs.h f2fs_fs.h jfs_superblock.h jfs.h gfs2.h hfs.h hfsp.h hpfs.h hfsp_struct.h luks.h luks_struct.h lvm.h md.h netware.h ntfs.h ntfs_struct.h refs.h rfs.h savehdr.h sun.h swap.h sysv.h ufs.h vmfs.h wbfs.h xfs.h xfs_struct.h zfs.h
diff --git a/src/file_sig.c b/src/file_sig.c
index 1b685b1e..65339598 100644
--- a/src/file_sig.c
+++ b/src/file_sig.c
@@ -45,6 +45,72 @@
 #include "common.h"
 #include "log.h"
 
+static int signature_cmp(const struct td_list_head *a, const struct td_list_head *b);
+
+#ifndef __FRAMAC__
+#include "list_add_sorted.h"
+/*@ requires compar == signature_cmp; */
+static inline void td_list_add_sorted(struct td_list_head *newe, struct td_list_head *head,
+    int (*compar)(const struct td_list_head *a, const struct td_list_head *b));
+#else
+/*@
+  @ requires \valid(newe);
+  @ requires \valid(head);
+  @ requires separation: \separated(newe, head);
+  @ requires list_separated(head->prev, newe);
+  @ requires list_separated(head, newe);
+  @ requires finite(head->prev);
+  @ requires finite(head);
+  @*/
+static inline void td_list_add_sorted_sig(struct td_list_head *newe, struct td_list_head *head)
+{
+  struct td_list_head *pos;
+  /*@
+    @ loop invariant \valid(pos);
+    @ loop invariant \valid(pos->prev);
+    @ loop invariant \valid(pos->next);
+    @ loop invariant pos == head || \separated(pos, head);
+    @ loop assigns pos;
+    @*/
+  td_list_for_each(pos, head)
+  {
+    /*@ assert \valid_read(newe); */
+    /*@ assert \valid_read(pos); */
+    if(signature_cmp(newe,pos)<0)
+      break;
+  }
+  if(pos != head)
+  {
+      __td_list_add(newe, pos->prev, pos);
+  }
+  else
+  {
+    /*@ assert finite(head->prev); */
+    /*@ assert finite(head); */
+    /*@ assert list_separated(head->prev, newe); */
+    /*@ assert list_separated(head, newe); */
+    td_list_add_tail(newe, head);
+  }
+}
+#endif
+
+#if 0
+/*@ requires valid_string_s: valid_read_string(s);
+  @ ensures  valid_string(\result);
+  @*/
+static char *td_strdup(const char *s)
+{
+  size_t l = strlen(s) + 1;
+  char *p = (char *)MALLOC(l);
+  /*@ assert valid_read_string(s); */
+  memcpy(p, s, l);
+  p[l-1]='\0';
+  /*@ assert valid_read_string(p); */
+  return p;
+}
+#endif
+
+/*@ requires valid_register_header_check(file_stat); */
 static void register_header_check_sig(file_stat_t *file_stat);
 
 const file_hint_t file_hint_sig= {
@@ -65,7 +131,7 @@ struct signature_s
 {
   struct td_list_head list;
   const char *extension;
-  const unsigned char *sig;
+  const char *sig;
   unsigned int sig_size;
   unsigned int offset;
 };
@@ -86,21 +152,25 @@ static signature_t signatures={
   .list = TD_LIST_HEAD_INIT(signatures.list)
 };
 
-#ifndef __FRAMAC__
-static
-#endif
-int signature_cmp(const struct td_list_head *a, const struct td_list_head *b)
+/*@
+  @ assigns \nothing;
+  @*/
+static int signature_cmp(const struct td_list_head *a, const struct td_list_head *b)
 {
   const signature_t *sig_a=td_list_entry_const(a, const signature_t, list);
   const signature_t *sig_b=td_list_entry_const(b, const signature_t, list);
   int res;
+  /*@ assert \valid_read(sig_a); */
+  /*@ assert \valid_read(sig_b); */
   /*@ assert valid_signature(sig_a); */
   /*@ assert valid_signature(sig_b); */
   if(sig_a->sig_size==0 && sig_b->sig_size!=0)
     return -1;
   if(sig_a->sig_size!=0 && sig_b->sig_size==0)
     return 1;
-  res=sig_a->offset-sig_b->offset;
+  /*@ assert 0 <= sig_a->offset <= PHOTOREC_MAX_SIG_OFFSET; */
+  /*@ assert 0 <= sig_b->offset <= PHOTOREC_MAX_SIG_OFFSET; */
+  res=(int)sig_a->offset - (int)sig_b->offset;
   if(res!=0)
     return res;
   if(sig_a->sig_size<=sig_b->sig_size)
@@ -133,8 +203,9 @@ static void signature_insert(const char *ext, unsigned int offset, const void*si
   /*@ assert \valid_read((const char *)sig+(0..sig_size-1)); */
   /*@ assert valid_read_string(ext); */
   newsig=(signature_t*)MALLOC(sizeof(*newsig));
+  /*@ assert \valid(newsig); */
   newsig->extension=ext;
-  newsig->sig=(const unsigned char *)sig;
+  newsig->sig=(const char *)sig;
   newsig->sig_size=sig_size;
   newsig->offset=offset;
   /*@ assert newsig->sig_size == sig_size; */
@@ -153,7 +224,11 @@ static void signature_insert(const char *ext, unsigned int offset, const void*si
   /*@ assert \valid_read((const char *)newsig->sig+(0..newsig->sig_size-1)); */
 
   /*@ assert valid_signature(newsig); */
+#ifdef __FRAMAC__
+  td_list_add_sorted_sig(&newsig->list, &signatures.list);
+#else
   td_list_add_sorted(&newsig->list, &signatures.list, signature_cmp);
+#endif
 }
 
 /*@
@@ -165,10 +240,14 @@ static void signature_insert(const char *ext, unsigned int offset, const void*si
 static int header_check_sig(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)
 {
   struct td_list_head *pos;
-  /*@ loop assigns pos; */
+  /*@
+    @ loop invariant \valid(pos);
+    @ loop assigns pos;
+    @*/
   td_list_for_each(pos, &signatures.list)
   {
     const signature_t *sig = td_list_entry(pos, signature_t, list);
+    /*@ assert \valid_read(sig); */
     /*@ assert sig->offset + sig->sig_size <= buffer_size; */
     /*@ assert valid_read_string(sig->extension); */
     /*@ assert valid_signature(sig); */
diff --git a/src/filegen.c b/src/filegen.c
index 7354382c..d680f352 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -46,6 +46,57 @@
 #include "filegen.h"
 #include "log.h"
 
+static int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b);
+
+#ifndef __FRAMAC__
+#include "list_add_sorted.h"
+/*@ requires compar == file_check_cmp; */
+static inline void td_list_add_sorted(struct td_list_head *newe, struct td_list_head *head,
+    int (*compar)(const struct td_list_head *a, const struct td_list_head *b));
+#else
+
+/*@
+  @ requires \valid(newe);
+  @ requires \valid(head);
+  @ requires separation: \separated(newe, head);
+  @ requires list_separated(head->prev, newe);
+  @ requires list_separated(head, newe);
+  @ requires finite(head->prev);
+  @ requires finite(head);
+  @*/
+static inline void td_list_add_sorted_fcc(struct td_list_head *newe, struct td_list_head *head)
+{
+  struct td_list_head *pos;
+  /*@
+    @ loop invariant \valid(pos);
+    @ loop invariant \valid(pos->prev);
+    @ loop invariant \valid(pos->next);
+    @ loop invariant pos == head || \separated(pos, head);
+    @ loop assigns pos;
+    @*/
+  td_list_for_each(pos, head)
+  {
+    /*@ assert \valid_read(newe); */
+    /*@ assert \valid_read(pos); */
+    if(file_check_cmp(newe,pos)<0)
+      break;
+  }
+  if(pos != head)
+  {
+      __td_list_add(newe, pos->prev, pos);
+  }
+  else
+  {
+    /*@ assert finite(head->prev); */
+    /*@ assert finite(head); */
+    /*@ assert list_separated(head->prev, newe); */
+    /*@ assert list_separated(head, newe); */
+    td_list_add_tail(newe, head);
+  }
+}
+#endif
+
+
 uint64_t gpls_nbr=0;
 static uint64_t offset_skipped_header=0;
 
@@ -57,16 +108,12 @@ file_check_list_t file_check_list={
     .list = TD_LIST_HEAD_INIT(file_check_list.list)
 };
 
-//  X requires \valid_read(b);
 /*@
   @ requires \valid_read(a);
   @ requires \valid_read(b);
   @ assigns \nothing;
   @*/
-#ifndef DISABLED_FOR_FRAMAC
-static
-#endif
-int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b)
+static int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b)
 {
 #ifdef DISABLED_FOR_FRAMAC
   return 1;
@@ -149,6 +196,7 @@ void register_header_check(const unsigned int offset, const void *value, const u
     file_stat_t *file_stat)
 {
   file_check_t *file_check_new=(file_check_t *)MALLOC(sizeof(*file_check_new));
+  /*@ assert \valid(file_check_new); */
   file_check_new->value=value;
   file_check_new->length=length;
   file_check_new->offset=offset;
@@ -166,7 +214,11 @@ void register_header_check(const unsigned int offset, const void *value, const u
   /*@ assert \valid(file_check_new->file_stat); */
 
   /*@ assert valid_file_check_node(file_check_new); */
+#ifdef __FRAMAC__
+  td_list_add_sorted_fcc(&file_check_new->list, &file_check_plist.list);
+#else
   td_list_add_sorted(&file_check_new->list, &file_check_plist.list, file_check_cmp);
+#endif
 }
 
 /*@
@@ -187,9 +239,14 @@ static void index_header_check_aux(file_check_t *file_check_new)
       if(pos->offset >= file_check_new->offset &&
 	  pos->offset < file_check_new->offset+file_check_new->length)
       {
+#ifdef __FRAMAC__
+	td_list_add_sorted_fcc(&file_check_new->list,
+	    &pos->file_checks[((const unsigned char *)file_check_new->value)[pos->offset-file_check_new->offset]].list);
+#else
 	td_list_add_sorted(&file_check_new->list,
 	    &pos->file_checks[((const unsigned char *)file_check_new->value)[pos->offset-file_check_new->offset]].list,
 	    file_check_cmp);
+#endif
 	return ;
       }
       if(pos->offset>file_check_new->offset)
@@ -319,6 +376,7 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
   memset(&buffer[4096],0,footer_length-1);
   /*@
     @ loop invariant 0 <= offset <= \at(offset, Pre);
+    @ loop invariant offset <= PHOTOREC_MAX_FILE_SIZE;
     @ loop assigns errno, *handle, Frama_C_entropy_source;
     @ loop assigns offset, buffer[0 .. 8192-1];
     @ loop variant offset;
@@ -333,6 +391,7 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
       offset-=4096;
     else
       offset=offset-(offset%4096);
+    /*@ assert offset + 4096 <= PHOTOREC_MAX_FILE_SIZE; */
     if(my_fseek(handle,offset,SEEK_SET)<0)
       return 0;
     taille=fread(&buffer, 1, 4096, handle);
@@ -342,9 +401,13 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
 #ifdef __FRAMAC__
     Frama_C_make_unknown(&buffer, 4096);
 #endif
-    /*@ loop assigns i; */
+    /*@
+      @ loop invariant -1 <= i < taille;
+      @ loop assigns i;
+      @*/
     for(i=taille-1;i>=0;i--)
     {
+      /*@ assert offset + i <= PHOTOREC_MAX_FILE_SIZE; */
       if(buffer[i]==*(const char *)footer && memcmp(&buffer[i],footer,footer_length)==0)
       {
         return offset + i;
@@ -357,17 +420,25 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
 
 void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length)
 {
+  /*@ assert \valid(file_recovery); */
   if(footer_length==0 || file_recovery->file_size <= extra_length)
     return ;
   file_recovery->file_size=file_rsearch(file_recovery->handle, file_recovery->file_size-extra_length, footer, footer_length);
+  /*@ assert 0 < footer_length < 4096; */
+  /*@ assert extra_length <= PHOTOREC_MAX_FILE_SIZE; */
+  /*@ assert file_recovery->file_size < 0x8000000000000000; */
   if(file_recovery->file_size > 0)
-    file_recovery->file_size+= footer_length + extra_length;
+    file_recovery->file_size+= (uint64_t)footer_length + extra_length;
   /*@ assert \valid(file_recovery->handle); */
   /*@ assert valid_file_check_result(file_recovery); */
 }
 
 data_check_t data_check_size(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
 {
+  /*@ assert \valid_read(file_recovery); */
+  /*@ assert valid_file_recovery(file_recovery); */
+  /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
+  /*@ assert buffer_size <= 2 * PHOTOREC_MAX_BLOCKSIZE; */
   if(file_recovery->file_size + buffer_size/2 >= file_recovery->calculated_file_size)
   {
     /*@ assert valid_file_recovery(file_recovery); */
@@ -379,6 +450,7 @@ data_check_t data_check_size(const unsigned char *buffer, const unsigned int buf
 
 void file_check_size(file_recovery_t *file_recovery)
 {
+  /*@ assert \valid(file_recovery); */
   if(file_recovery->file_size<file_recovery->calculated_file_size)
     file_recovery->file_size=0;
   else
@@ -388,6 +460,7 @@ void file_check_size(file_recovery_t *file_recovery)
 
 void file_check_size_min(file_recovery_t *file_recovery)
 {
+  /*@ assert \valid(file_recovery); */
   if(file_recovery->file_size<file_recovery->calculated_file_size)
     file_recovery->file_size=0;
   /*@ assert valid_file_check_result(file_recovery); */
@@ -395,6 +468,7 @@ void file_check_size_min(file_recovery_t *file_recovery)
 
 void file_check_size_max(file_recovery_t *file_recovery)
 {
+  /*@ assert \valid(file_recovery); */
   if(file_recovery->file_size > file_recovery->calculated_file_size)
     file_recovery->file_size=file_recovery->calculated_file_size;
   /*@ assert valid_file_check_result(file_recovery); */
@@ -528,11 +602,14 @@ static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
 
 /*@
   @ requires \valid(file_recovery);
+  @ requires strlen((char*)&file_recovery->filename) < 1<<30;
+  @ requires valid_file_recovery(file_recovery);
   @ requires valid_read_string((char*)&file_recovery->filename);
   @ requires 0 <= offset < buffer_size;
+  @ requires buffer_size < 1<<30;
   @ requires \valid_read((char *)buffer+(0..buffer_size-1));
-  @ requires new_ext==\null || valid_read_string(new_ext);
-  @ ensures  new_ext==\null || valid_read_string(new_ext);
+  @ requires new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
+  @ ensures  new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
   @ ensures  valid_file_recovery(file_recovery);
   @*/
 static 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)
@@ -542,7 +619,7 @@ static int _file_rename(file_recovery_t *file_recovery, const void *buffer, cons
   const char *ext=NULL;
   char *dst;
   char *directory_sep;
-  int len;
+  size_t len;
   len=strlen(src)+1;
   /*@ assert offset < buffer_size; */
   len+=buffer_size-offset+1;
@@ -667,11 +744,14 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
 /* The original filename begins at offset in buffer and is null terminated */
 /*@
   @ requires \valid(file_recovery);
+  @ requires strlen((char*)&file_recovery->filename) < 1<<30;
   @ requires valid_file_recovery(file_recovery);
   @ requires valid_read_string((char*)&file_recovery->filename);
   @ requires 0 <= offset < buffer_size;
+  @ requires buffer_size < 1<<30;
   @ requires \valid_read((char *)buffer+(0..buffer_size-1));
-  @ requires new_ext==\null || valid_read_string(new_ext);
+  @ requires new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
+  @ ensures  new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
   @ ensures  valid_read_string((char*)&file_recovery->filename);
   @ ensures  valid_file_recovery(file_recovery);
   @*/
@@ -682,7 +762,7 @@ static int _file_rename_unicode(file_recovery_t *file_recovery, const void *buff
   const char *src_ext=src;
   char *dst;
   char *dst_dir_sep;
-  int len=strlen(src)+1;
+  size_t len=strlen(src)+1;
   /*@ assert offset < buffer_size; */
   len+=buffer_size-offset;
   if(new_ext!=NULL)
@@ -855,6 +935,7 @@ int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery
 }
 
 /*@
+  @ requires file_recovery_new == \null || \valid_read(file_recovery_new);
   @ requires \separated(file_recovery_new, &offset_skipped_header);
   @ assigns offset_skipped_header;
   @*/
@@ -865,6 +946,7 @@ void header_ignored(const file_recovery_t *file_recovery_new)
     offset_skipped_header=0;
     return ;
   }
+  /*@ assert \valid_read(file_recovery_new); */
   if(file_recovery_new->location.start < offset_skipped_header || offset_skipped_header==0)
     offset_skipped_header=file_recovery_new->location.start;
 }
@@ -878,13 +960,18 @@ void get_prev_location_smart(const alloc_data_t *list_search_space, alloc_data_t
   alloc_data_t *file_space=*current_search_space;
   if(offset_skipped_header==0)
     return ;
+#ifndef __FRAMAC__
   gpls_nbr++;
+#endif
   /*@
+    @ loop invariant \valid_read(file_space);
+    @ loop invariant \separated(file_space, current_search_space, offset);
     @ loop assigns file_space, offset_skipped_header, *current_search_space, *offset;
     @*/
   while(1)
   {
     file_space=td_list_prev_entry(file_space, list);
+    /*@ assert \valid_read(file_space); */
     if(file_space==list_search_space)
       break;
     if(file_space->start <= offset_skipped_header && offset_skipped_header < file_space->end)
@@ -903,11 +990,14 @@ void get_prev_location_smart(const alloc_data_t *list_search_space, alloc_data_t
       (long long unsigned)(*offset/512));
 #endif
   /*@
+    @ loop invariant \valid_read(file_space);
+    @ loop invariant \separated(file_space, current_search_space, offset);
     @ loop assigns file_space, offset_skipped_header, *current_search_space, *offset;
     @*/
   while(1)
   {
     file_space=td_list_prev_entry(file_space, list);
+    /*@ assert \valid_read(file_space); */
     if(file_space==list_search_space)
     {
       offset_skipped_header=0;
diff --git a/src/list.h b/src/list.h
index dc0e63b0..201ec060 100644
--- a/src/list.h
+++ b/src/list.h
@@ -21,6 +21,7 @@
  */
 #ifndef _LIST_H
 #define _LIST_H
+
 /*
  * These are non-NULL pointers that will result in page faults
  * under normal circumstances, used to verify that nobody uses
@@ -44,37 +45,42 @@ struct td_list_head {
 	struct td_list_head *next, *prev;
 };
 
-#ifdef __FRAMAC__
 /*@
-  @ requires \valid_read(a);
-  @ requires \valid_read(b);
-  @ assigns \nothing;
-  @*/
-int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b);
-
-/*@
-  @ assigns \nothing;
-  @*/
-int signature_cmp(const struct td_list_head *a, const struct td_list_head *b);
-#endif
-
-/*@
-  inductive reachable{L}(struct td_list_head *root, struct td_list_head *node) {
-    case root_reachable{L}:
-      \forall struct td_list_head *root; reachable(root,root) ;
+  inductive reachable_forward{L}(struct td_list_head *root, struct td_list_head *node) {
+    case root_reachable_forward{L}:
+      \forall struct td_list_head *root; reachable_forward(root,root) ;
     case next_reachable{L}:
       \forall struct td_list_head *root,*node;
-      \valid(root) && reachable(root->next,node) ==> reachable(root,node);
+      \valid(root) && reachable_forward(root->next,node) ==> reachable_forward(root,node);
+  }
+
+  inductive reachable_backward{L}(struct td_list_head *root, struct td_list_head *node) {
+    case root_reachable_backward{L}:
+      \forall struct td_list_head *root; reachable_backward(root,root) ;
+    case prev_reachable{L}:
+      \forall struct td_list_head *root,*node;
+      \valid(root) && reachable_backward(root->prev,node) ==> reachable_backward(root,node);
   }
   @*/
   // root->next->prev == root
 
-/*@ predicate finite{L}(struct td_list_head *root) = reachable(root->next,root); */
+/*@ predicate finite{L}(struct td_list_head *root) = reachable_forward(root->next,root) && reachable_backward(root->prev,root); */
+
 
 /*
       \forall struct td_list_head *l1;
         reachable(l, l1) && \valid(l1) ==> \valid(l1->next) && l1->next->prev == l1;
 */
+/*@ inductive list_separated3{L}(struct td_list_head *root, struct td_list_head *node, struct td_list_head *elt) {
+     case node_is_root{L}:
+       \forall struct td_list_head *root, *elt; \separated(root, elt) ==> list_separated3(root, root, elt);
+     case node_reachable{L}:
+       \forall struct td_list_head *root, *node, *elt;
+       \valid(node) && \separated(node, elt) && list_separated3(root, node->next, elt) ==> list_separated3(root, node, elt);
+ }
+
+ */
+/*@ predicate list_separated{L}(struct td_list_head *root, struct td_list_head *elt) = list_separated3(root, root->next, elt); */
 
 #define TD_LIST_HEAD_INIT(name) { &(name), &(name) }
 
@@ -97,10 +103,16 @@ int signature_cmp(const struct td_list_head *a, const struct td_list_head *b);
   @ requires \valid(next);
   @ requires separation: \separated(newe, \union(prev,next));
   @ requires prev == next || \separated(prev,next,newe);
-  @ ensures next->prev == newe;
-  @ ensures newe->next == next;
-  @ ensures newe->prev == prev;
+  @ requires finite(prev);
+  @ requires finite(next);
+  @ requires prev->next == next;
+  @ requires next->prev == prev;
+  @ requires list_separated(prev, newe);
+  @ requires list_separated(next, newe);
   @ ensures prev->next == newe;
+  @ ensures newe->prev == prev;
+  @ ensures newe->next == next;
+  @ ensures next->prev == newe;
   @ ensures newe->next->prev == newe;
   @ ensures newe->prev->next == newe;
   @ assigns next->prev,newe->next,newe->prev,prev->next;
@@ -109,14 +121,24 @@ static inline void __td_list_add(struct td_list_head *newe,
 			      struct td_list_head *prev,
 			      struct td_list_head *next)
 {
+        /*@ assert finite(prev); */
+        /*@ assert finite(next); */
+        /*@ assert reachable_forward(prev->next,prev); */
+        /*@ assert reachable_forward(next->next,next); */
+        /*@ assert reachable_backward(prev->prev,prev); */
+        /*@ assert reachable_backward(next->prev,next); */
+
+        /*@ assert reachable_forward(next,prev); */
 	newe->next = next;
 	newe->prev = prev;
-	next->prev = newe;
 	prev->next = newe;
+	next->prev = newe;
 	/*@ assert next->prev == newe; */
 	/*@ assert newe->next == next; */
 	/*@ assert newe->prev == prev; */
 	/*@ assert prev->next == newe; */
+	/*@ assert reachable_forward(prev,newe); */
+	/*@ assert reachable_backward(next,newe); */
 }
 
 /**
@@ -132,6 +154,9 @@ static inline void __td_list_add(struct td_list_head *newe,
   @ requires \valid(head);
   @ requires \valid(head->next);
   @ requires separation: \separated(newe, \union(head,head->next));
+  @ requires finite(head);
+  @ requires finite(head->next);
+  @ requires list_separated(head, newe);
   @ ensures head->next == newe;
   @ ensures newe->prev == head;
   @ ensures newe->next == \old(head->next);
@@ -155,8 +180,13 @@ static inline void td_list_add(struct td_list_head *newe, struct td_list_head *h
   @ requires \valid(newe);
   @ requires \valid(head);
   @ requires \valid(head->prev);
+  @ requires separation: \separated(newe, head);
   @ requires \separated(newe, \union(head->prev, head));
   @ requires head->prev == head || \separated(head->prev, head, newe);
+  @ requires finite(head->prev);
+  @ requires list_separated(head->prev, newe);
+  @ requires list_separated(head, newe);
+  @ requires finite(head);
   @ ensures head->prev == newe;
   @ ensures newe->next == head;
   @ ensures newe->prev == \old(head->prev);
@@ -218,6 +248,7 @@ static inline void td_list_del(struct td_list_head *entry)
 	/*@ assert \at(entry->next,Pre)->prev == \at(entry->prev,Pre); */
 }
 
+#if 0
 /**
  * td_list_del_init - deletes entry from list and reinitialize it.
  * @entry: the element to delete from the list.
@@ -227,7 +258,9 @@ static inline void td_list_del_init(struct td_list_head *entry)
 	__td_list_del(entry->prev, entry->next);
 	TD_INIT_LIST_HEAD(entry);
 }
+#endif
 
+#if 0
 /**
  * td_list_move - delete from one list and add as another's head
  * @list: the entry to move
@@ -250,6 +283,7 @@ static inline void td_list_move_tail(struct td_list_head *list,
         __td_list_del(list->prev, list->next);
         td_list_add_tail(list, head);
 }
+#endif
 
 /**
  * td_list_empty - tests whether a list is empty
@@ -264,6 +298,7 @@ static inline int td_list_empty(const struct td_list_head *head)
 	return head->next == head;
 }
 
+#if 0
 /**
  * td_list_empty_careful - tests whether a list is
  * empty _and_ checks that no other CPU might be
@@ -322,6 +357,7 @@ static inline void td_list_splice_init(struct td_list_head *list,
 		TD_INIT_LIST_HEAD(list);
 	}
 }
+#endif
 
 /**
  * td_list_entry - get the struct for this entry
@@ -473,67 +509,6 @@ static inline void td_list_splice_init(struct td_list_head *list,
 	td_list_entry((pos)->member.prev, typeof(*(pos)), member)
 
 
-/*@
-  @ requires \valid(newe);
-  @ requires \valid(head);
-  @ requires \valid_function(compar);
-  @ requires compar == signature_cmp || compar == file_check_cmp;
-  @ requires separation: \separated(newe, head);
-  @*/
-static inline void td_list_add_sorted(struct td_list_head *newe, struct td_list_head *head,
-    int (*compar)(const struct td_list_head *a, const struct td_list_head *b))
-{
-  struct td_list_head *pos;
-  /*@
-    @ loop invariant pos == head || \separated(pos, head);
-    @ loop invariant compar == signature_cmp || compar == file_check_cmp;
-    @*/
-  td_list_for_each(pos, head)
-  {
-    /*@ assert compar == signature_cmp || compar == file_check_cmp; */
-    /*@ assert \valid_read(newe); */
-    /*@ assert \valid_read(pos); */
-    if(compar(newe,pos)<0)
-    {
-      __td_list_add(newe, pos->prev, pos);
-      return ;
-    }
-  }
-  td_list_add_tail(newe, head);
-}
-
-/*@
-  @ requires \valid(newe);
-  @ requires \valid(head);
-  @ requires \valid_function(compar);
-  @ requires separation: \separated(newe, head);
-  @*/
-static inline int td_list_add_sorted_uniq(struct td_list_head *newe, struct td_list_head *head,
-    int (*compar)(const struct td_list_head *a, const struct td_list_head *b))
-{
-  struct td_list_head *pos;
-  /*@
-    @ loop invariant pos == head || \separated(pos, head);
-    @ loop invariant \valid_function(compar);
-    @ loop assigns pos;
-    @*/
-  td_list_for_each(pos, head)
-  {
-    // TODO const
-    /* calls spacerange_cmp; */
-    int res=compar(newe,pos);
-    if(res<0)
-    {
-      __td_list_add(newe, pos->prev, pos);
-      return 0;
-    }
-    else if(res==0)
-      return 1;
-  }
-  td_list_add_tail(newe, head);
-  return 0;
-}
-
 typedef struct alloc_list_s alloc_list_t;
 struct alloc_list_s
 {
diff --git a/src/list_add_sorted.h b/src/list_add_sorted.h
new file mode 100644
index 00000000..a33a7f3c
--- /dev/null
+++ b/src/list_add_sorted.h
@@ -0,0 +1,80 @@
+/*
+
+    File: list_add_sorted.h
+
+    Copyright (C) 2006-2008 Christophe GRENIER <grenier@cgsecurity.org>
+
+    This software is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write the Free Software Foundation, Inc., 51
+    Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+ */
+#ifndef _LIST_ADD_SORTED_UNIQ_H
+#define _LIST_ADD_SORTED_UNIQ_H
+
+/*
+  X requires finite(head);
+  X ensures  finite(head);
+  X ensures  finite(newe);
+  X ensures  reachable(head,newe);
+  */
+/*@
+  @ requires \valid(newe);
+  @ requires \valid(head);
+  @ requires \valid_function(compar);
+  @ requires separation: \separated(newe, head);
+  @ requires list_separated(head->prev, newe);
+  @ requires list_separated(head, newe);
+  @ requires finite(head->prev);
+  @ requires finite(head);
+  @*/
+static inline void td_list_add_sorted(struct td_list_head *newe, struct td_list_head *head,
+    int (*compar)(const struct td_list_head *a, const struct td_list_head *b))
+{
+  struct td_list_head *pos;
+  /*@
+    @ loop invariant \valid(pos);
+    @ loop invariant \valid(pos->prev);
+    @ loop invariant \valid(pos->next);
+    @ loop invariant pos == head || \separated(pos, head);
+    @ loop invariant \valid_function(compar);
+    @ loop assigns pos;
+    @*/
+/*
+    X loop invariant finite(head->prev);
+    X loop invariant finite(head);
+*/
+  td_list_for_each(pos, head)
+  {
+    /*@ assert \valid_function(compar); */
+    /*@ assert \valid_read(newe); */
+    /*@ assert \valid_read(pos); */
+    if(compar(newe,pos)<0)
+      break;
+  }
+  if(pos != head)
+  {
+      __td_list_add(newe, pos->prev, pos);
+  }
+  else
+  {
+    /*@ assert finite(head->prev); */
+    /*@ assert finite(head); */
+    /*@ assert list_separated(head->prev, newe); */
+    /*@ assert list_separated(head, newe); */
+    td_list_add_tail(newe, head);
+  }
+  /*X assert finite(head); */
+  /*X assert finite(newe); */
+}
+#endif
diff --git a/src/list_add_sorted_uniq.h b/src/list_add_sorted_uniq.h
new file mode 100644
index 00000000..936fac76
--- /dev/null
+++ b/src/list_add_sorted_uniq.h
@@ -0,0 +1,74 @@
+/*
+
+    File: list_add_sorted_uniq.h
+
+    Copyright (C) 2006-2008 Christophe GRENIER <grenier@cgsecurity.org>
+
+    This software is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write the Free Software Foundation, Inc., 51
+    Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+ */
+#ifndef _LIST_ADD_SORTED_UNIQ_H
+#define _LIST_ADD_SORTED_UNIQ_H
+
+/*@
+  @ requires \valid(newe);
+  @ requires \valid(head);
+  @ requires \valid_function(compar);
+  @ requires finite(head->prev);
+  @ requires finite(head);
+  @ requires separation: \separated(newe, head);
+  @ requires list_separated(head, newe);
+  @*/
+static inline int td_list_add_sorted_uniq(struct td_list_head *newe, struct td_list_head *head,
+    int (*compar)(const struct td_list_head *a, const struct td_list_head *b))
+{
+  struct td_list_head *pos;
+  /*@
+    @ loop invariant \valid(pos);
+    @ loop invariant \valid(pos->prev);
+    @ loop invariant \valid(pos->next);
+    @ loop invariant pos == head || \separated(pos, head);
+    @ loop invariant \valid_function(compar);
+    @ loop invariant finite(head->prev);
+    @ loop invariant finite(head);
+    @ loop invariant finite(pos->prev);
+    @ loop invariant finite(pos);
+    @ loop assigns pos;
+    @*/
+  td_list_for_each(pos, head)
+  {
+    /*@ assert \valid_function(compar); */
+    // TODO const
+    /* calls spacerange_cmp; */
+    int res=compar(newe,pos);
+    /*@ assert \valid(pos); */
+    /*@ assert \valid(pos->prev); */
+    /*@ assert \valid(pos->next); */
+    if(res<0)
+    {
+      __td_list_add(newe, pos->prev, pos);
+      return 0;
+    }
+    else if(res==0)
+      return 1;
+  }
+  /*@ assert finite(head->prev); */
+  /*@ assert finite(head); */
+  /*@ assert list_separated(head->prev, newe); */
+  /*@ assert list_separated(head, newe); */
+  td_list_add_tail(newe, head);
+  return 0;
+}
+#endif
diff --git a/src/phcli.c b/src/phcli.c
index e8830663..e0153471 100644
--- a/src/phcli.c
+++ b/src/phcli.c
@@ -42,6 +42,7 @@ extern int need_to_stop;
 #include "geometry.h"
 #include "poptions.h"
 #include "phcli.h"
+#include "list_add_sorted_uniq.h"
 
 typedef enum { INIT_SPACE_WHOLE, INIT_SPACE_PREINIT, INIT_SPACE_EXT2_GROUP, INIT_SPACE_EXT2_INODE } init_mode_t;