1 files changed, 39 insertions, 6 deletions

diff --git a/src/photorec_check_header.h b/src/photorec_check_header.h
index 203641eb..a13ba3ce 100644
--- a/src/photorec_check_header.h
+++ b/src/photorec_check_header.h
@@ -61,6 +61,9 @@ static FILE *fopen_with_retry(const char *path, const char *mode)
 }
 #endif
 
+/*@
+  @ requires \valid_read(buffer + (0 .. read_size-1));
+  @*/
 static void photorec_dir_fat(const unsigned char *buffer, const unsigned int read_size, const unsigned long long sector)
 {
   file_info_t dir_list;
@@ -68,7 +71,9 @@ static void photorec_dir_fat(const unsigned char *buffer, const unsigned int rea
   dir_fat_aux(buffer, read_size, 0, &dir_list);
   if(!td_list_empty(&dir_list.list))
   {
+#ifndef __FRAMAC__
     log_info("Sector %llu\n", sector);
+#endif
     dir_aff_log(NULL, &dir_list);
     delete_list_file(&dir_list);
   }
@@ -76,20 +81,19 @@ static void photorec_dir_fat(const unsigned char *buffer, const unsigned int rea
 
 /*@
   @ requires \valid_read(file_recovery_new);
+  @ requires valid_file_recovery(file_recovery_new);
   @ requires \valid(file_recovery);
-  @ requires file_recovery->extension == \null || valid_read_string(file_recovery->extension);
-  @ requires \valid(file_recovery->file_stat);
-  @ requires \valid(file_recovery->file_stat->file_hint);
-  @ requires valid_read_string(file_recovery->file_stat->file_hint->description);
+  @ requires valid_file_recovery(file_recovery);
   @ requires \valid(params);
   @ requires \valid(params->disk);
   @ requires \valid_read(options);
   @ requires \valid(list_search_space);
-  @ requires \valid(buffer + (0 .. params->blocksize -1));
+  @ requires \valid_read(buffer + (0 .. params->blocksize -1));
   @ requires params->disk->sector_size > 0;
+  @ requires \separated(file_recovery_new, file_recovery, params, options, list_search_space, buffer+(..), file_recovered, &errno);
   @ ensures \result == PSTATUS_OK || \result == PSTATUS_EACCES;
-  @ ensures *file_recovered == PFSTATUS_BAD || *file_recovered == PFSTATUS_OK || *file_recovered == PFSTATUS_OK_TRUNCATED;
   @*/
+// ensures *file_recovered == PFSTATUS_BAD || *file_recovered == PFSTATUS_OK || *file_recovered == PFSTATUS_OK_TRUNCATED;
 static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new, file_recovery_t *file_recovery, struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space, const unsigned char *buffer, pfstatus_t *file_recovered, const uint64_t offset)
 {
   *file_recovered=PFSTATUS_BAD;
@@ -97,13 +101,17 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new,
     return PSTATUS_OK;
   if(file_recovery->file_stat!=NULL)
   {
+    /*@ assert valid_file_stat(file_recovery->file_stat); */
+#ifndef __FRAMAC__
     if(options->verbose > 1)
       log_trace("A known header has been found, recovery of the previous file is finished\n");
+#endif
     *file_recovered=file_finish2(file_recovery, params, options->paranoid, list_search_space);
     if(*file_recovered==PFSTATUS_OK_TRUNCATED)
       return PSTATUS_OK;
   }
   file_recovery_cpy(file_recovery, file_recovery_new);
+#ifndef __FRAMAC__
   if(options->verbose > 1)
   {
     log_info("%s header found at sector %lu\n",
@@ -113,12 +121,15 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new,
     log_info("file_recovery->location.start=%lu\n",
 	(unsigned long)(file_recovery->location.start/params->disk->sector_size));
   }
+#endif
+#ifndef __FRAMAC__
   if(file_recovery->file_stat->file_hint==&file_hint_dir && options->verbose > 0)
   { /* FAT directory found, list the file */
     const unsigned int blocksize=params->blocksize;
     const unsigned int read_size=(blocksize>65536?blocksize:65536);
     photorec_dir_fat(buffer, read_size, file_recovery->location.start/params->disk->sector_size);
   }
+#endif
   set_filename(file_recovery, params);
   if(file_recovery->file_stat->file_hint->recover==1)
   {
@@ -129,7 +140,9 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new,
 #endif
     if(!file_recovery->handle)
     {
+#ifndef __FRAMAC__
       log_critical("Cannot create file %s: %s\n", file_recovery->filename, strerror(errno));
+#endif
       params->offset=offset;
       return PSTATUS_EACCES;
     }
@@ -137,26 +150,43 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new,
   return PSTATUS_OK;
 }
 
+/*@
+  @ requires \valid(file_recovery);
+  @ requires valid_file_recovery(file_recovery);
+  @ requires \valid(params);
+  @ requires valid_ph_param(params);
+  @ requires \valid_read(options);
+  @ requires valid_list_search_space(list_search_space);
+  @ requires \valid_read(buffer + (0 .. params->blocksize -1));
+  @ requires \valid(file_recovered);
+  @ requires \separated(file_recovery, params, options, list_search_space, buffer, file_recovered);
+  @ ensures  valid_file_recovery(file_recovery);
+  @*/
+// ensures  valid_list_search_space(list_search_space);
 inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space, const unsigned char *buffer, pfstatus_t *file_recovered, const uint64_t offset)
 {
   const struct td_list_head *tmpl;
   const unsigned int blocksize=params->blocksize;
   const unsigned int read_size=(blocksize>65536?blocksize:65536);
   file_recovery_t file_recovery_new;
+  /*@ assert valid_file_recovery(file_recovery); */
   file_recovery_new.blocksize=blocksize;
   file_recovery_new.location.start=offset;
   if(file_recovery->file_stat!=NULL && file_recovery->file_stat->file_hint==&file_hint_tar &&
       is_valid_tar_header((const struct tar_posix_header *)(buffer-0x200)))
   { /* Currently saving a tar, do not check the data for know header */
+#ifndef __FRAMAC__
     if(options->verbose > 1)
     {
       log_verbose("Currently saving a tar file, sector %lu.\n",
 	  (unsigned long)((offset-params->partition->part_offset)/params->disk->sector_size));
     }
+#endif
     return PSTATUS_OK;
   }
   file_recovery_new.file_stat=NULL;
   file_recovery_new.location.start=offset;
+  /*@ loop invariant valid_file_recovery(file_recovery); */
   td_list_for_each(tmpl, &file_check_list.list)
   {
     const struct td_list_head *tmp;
@@ -164,10 +194,13 @@ inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, st
     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 \valid_function(file_check->header_check); */
+      /*@ assert valid_file_check_node(file_check); */
       if((file_check->length==0 || memcmp(buffer + file_check->offset, file_check->value, file_check->length)==0) &&
 	  file_check->header_check(buffer, read_size, 0, file_recovery, &file_recovery_new)!=0)
       {
 	file_recovery_new.file_stat=file_check->file_stat;
+	/*@ assert valid_file_recovery(&file_recovery_new); */
 	return photorec_header_found(&file_recovery_new, file_recovery, params, options, list_search_space, buffer, file_recovered, offset);
       }
     }