diff --git a/src/file_pf.c b/src/file_pf.c
index 8aab2f13..68dac3cb 100644
--- a/src/file_pf.c
+++ b/src/file_pf.c
@@ -31,6 +31,9 @@
 #include "types.h"
 #include "filegen.h"
 #include "common.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
 
 static void register_header_check_pf(file_stat_t *file_stat);
 
@@ -54,6 +57,10 @@ struct pf_header
   uint32_t unknown2;
 } __attribute__ ((gcc_struct, __packed__));
 
+/*@
+  @ requires \valid(file_recovery);
+  @ requires valid_read_string((char*)&file_recovery->filename);
+  @*/
 static void file_rename_pf(file_recovery_t *file_recovery)
 {
   FILE *file;
@@ -69,12 +76,29 @@ static void file_rename_pf(file_recovery_t *file_recovery)
   file_rename_unicode(file_recovery, &hdr.name, sizeof(hdr.name), 0, "pf", 0);
 }
 
+/*@
+  @ requires buffer_size >= sizeof(struct pf_header);
+  @ 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 separation: \separated(file_recovery, file_recovery_new);
+  @ ensures \result == 0 || \result == 1;
+  @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_pf.extension);
+  @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= sizeof(struct pf_header));
+  @ ensures (\result == 1) ==> (file_recovery_new->file_rename==&file_rename_pf);
+  @ ensures (\result == 1) ==> (file_recovery_new->data_check==&data_check_size);
+  @ ensures (\result == 1) ==> (file_recovery_new->file_check==&file_check_size);
+  @*/
 static int header_check_pf(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 pf_header *pf=(const struct pf_header *)buffer;
+  const unsigned int size=le32(pf->size);
+  if(size < sizeof(struct pf_header))
+    return 0;
   reset_file_recovery(file_recovery_new);
   file_recovery_new->extension=file_hint_pf.extension;
-  file_recovery_new->calculated_file_size=(uint64_t)le32(pf->size);
+  file_recovery_new->calculated_file_size=size;
   file_recovery_new->file_rename=&file_rename_pf;
   file_recovery_new->data_check=&data_check_size;
   file_recovery_new->file_check=&file_check_size;
@@ -86,3 +110,92 @@ static void register_header_check_pf(file_stat_t *file_stat)
   static const unsigned char pf_header[7] = {0x00, 0x00, 0x00, 'S', 'C', 'C', 'A'};
   register_header_check(1, pf_header,sizeof(pf_header), &header_check_pf, file_stat);
 }
+
+#if defined(MAIN_pf)
+#define BLOCKSIZE 65536u
+int main()
+{
+  const char *fn = "recup_dir.1/f0000000.pf";
+  unsigned char buffer[BLOCKSIZE];
+  file_recovery_t file_recovery_new;
+  file_recovery_t file_recovery;
+  file_stat_t file_stats;
+
+  /*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */
+#if defined(__FRAMAC__)
+  Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+
+  reset_file_recovery(&file_recovery);
+  file_recovery.blocksize=BLOCKSIZE;
+  file_recovery_new.blocksize=BLOCKSIZE;
+  file_recovery_new.data_check=NULL;
+  file_recovery_new.file_stat=NULL;
+  file_recovery_new.file_check=NULL;
+  file_recovery_new.file_rename=NULL;
+  file_recovery_new.calculated_file_size=0;
+  file_recovery_new.file_size=0;
+  file_recovery_new.location.start=0;
+
+  file_stats.file_hint=&file_hint_pf;
+  file_stats.not_recovered=0;
+  file_stats.recovered=0;
+  register_header_check_pf(&file_stats);
+  if(header_check_pf(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+    return 0;
+  /*@ assert valid_read_string(fn); */
+  strcpy(file_recovery_new.filename, fn);
+  /*@ assert file_recovery_new.file_size == 0;	*/
+  /*@ assert file_recovery_new.extension == file_hint_pf.extension; */
+  /*@ assert file_recovery_new.file_rename==&file_rename_pf; */
+  /*@ assert file_recovery_new.file_check == &file_check_size; */
+  /*@ assert file_recovery_new.data_check == &data_check_size; */
+  file_recovery_new.file_stat=&file_stats;
+  /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+  if(file_recovery_new.file_stat!=NULL && file_recovery_new.file_stat->file_hint!=NULL &&
+    file_recovery_new.data_check!=NULL)
+  {
+    unsigned char big_buffer[2*BLOCKSIZE];
+    data_check_t res_data_check=DC_CONTINUE;
+    memset(big_buffer, 0, BLOCKSIZE);
+    memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+    /*@ assert file_recovery_new.data_check == &data_check_size; */
+    /*@ assert file_recovery_new.file_size == 0; */;
+    res_data_check=data_check_size(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+    file_recovery_new.file_size+=BLOCKSIZE;
+    if(res_data_check == DC_CONTINUE)
+    {
+      memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+      Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+      data_check_size(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+    }
+  }
+  {
+    file_recovery_t file_recovery_new2;
+    /* Test when another file of the same is detected in the next block */
+    file_recovery_new2.blocksize=BLOCKSIZE;
+    file_recovery_new2.file_stat=NULL;
+    file_recovery_new2.file_check=NULL;
+    file_recovery_new2.location.start=BLOCKSIZE;
+    file_recovery_new.handle=NULL;	/* In theory should be not null */
+  #if defined(__FRAMAC__)
+    Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+  /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+    header_check_pf(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+  }
+  file_recovery_new.handle=fopen(fn, "rb");
+  /*@ assert file_recovery_new.file_check == &file_check_size; */
+  if(file_recovery_new.handle!=NULL)
+  {
+    file_check_size(&file_recovery_new);
+    fclose(file_recovery_new.handle);
+  }
+  /*@ assert file_recovery_new.file_rename==&file_rename_pf; */
+  /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+  file_rename_pf(&file_recovery_new);
+  return 0;
+}
+#endif