file_*.c: add various Frama-C annotations

src/file_ace.c

@@ -111,10 +111,8 @@ static int check_ace_crc(FILE *handle, const unsigned int len, const unsigned in
 }
 
 /*@
-  @ requires \valid(file_recovery);
+  @ requires valid_file_recovery(file_recovery);
   @ requires \valid(file_recovery->handle);
-  @ requires \valid_read(&file_recovery->extension);
-  @ requires valid_read_string(file_recovery->extension);
   @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
   @ requires \initialized(&file_recovery->time);
   @
@@ -143,9 +141,7 @@ static void file_check_ace(file_recovery_t *file_recovery)
     {
       return ;
     }
-#ifdef __FRAMAC__
+    /*@ assert \initialized(&buffer + (0 .. sizeof(buffer)-1)); */
-    Frama_C_make_unknown(&buffer, sizeof(buffer));
-#endif
 #ifdef DEBUG_ACE
     log_info("file_ace: Block header at 0x%08lx: CRC16=0x%04X size=%u type=%u"
         " flags=0x%04X addsize=%u\n",

src/file_amd.c

@@ -51,9 +51,9 @@ const file_hint_t file_hint_amd= {
   @ requires \valid(file_recovery_new);
   @ requires file_recovery_new->blocksize > 0;
   @ requires separation: \separated(&file_hint_amd, buffer+(..), file_recovery, file_recovery_new);
-  @ assigns  *file_recovery_new;
   @ ensures \result == 0 || \result == 1;
   @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
   @*/
 static int header_check_amd(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)
 {
@@ -73,9 +73,9 @@ static int header_check_amd(const unsigned char *buffer, const unsigned int buff
   @ requires \valid(file_recovery_new);
   @ requires file_recovery_new->blocksize > 0;
   @ requires separation: \separated(&file_hint_amd, buffer+(..), file_recovery, file_recovery_new);
-  @ assigns  *file_recovery_new;
   @ ensures \result == 0 || \result == 1;
   @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
   @*/
 static int header_check_amt(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)
 {

src/file_amr.c

@@ -94,8 +94,9 @@ static data_check_t data_check_amr(const unsigned char *buffer, const unsigned i
   @ requires \valid(file_recovery_new);
   @ requires file_recovery_new->blocksize > 0;
   @ requires separation: \separated(&file_hint_amr, buffer+(..), file_recovery, file_recovery_new);
-  @ assigns  *file_recovery_new;
+  @ ensures  \result == 0 || \result == 1;
   @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
   @*/
 static int header_check_amr(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)
 {

src/file_arj.c

@@ -119,13 +119,13 @@ struct arj_main_header {
 } __attribute__ ((gcc_struct, __packed__));
 
 /*@
+  @ requires \valid(file_recovery);
   @ requires valid_file_recovery(file_recovery);
   @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
   @ requires file_recovery->file_check == &file_check_arj;
+  @ ensures \valid(file_recovery->handle);
   @ assigns *file_recovery->handle, errno, file_recovery->file_size;
   @ assigns Frama_C_entropy_source;
-  @
-  @ ensures \valid(file_recovery->handle);
   @*/
 static void file_check_arj(file_recovery_t *file_recovery)
 {
@@ -134,14 +134,14 @@ static void file_check_arj(file_recovery_t *file_recovery)
 }
 
 /*@
-  @ requires buffer_size > sizeof(struct arj_main_header);
+  @ requires buffer_size >= sizeof(struct arj_main_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_arj, buffer+(..), file_recovery, file_recovery_new);
-  @ assigns  *file_recovery_new;
   @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
   @*/
 static int header_check_arj(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)
 {

src/file_bmp.c

@@ -99,10 +99,8 @@ struct bmp_header
   @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
   @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
   @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
-  @ ensures (\result == 1) ==>  \separated(file_recovery_new, file_recovery_new->extension);
-  @ ensures *buffer==\old(*buffer);
   @*/
-  /* TODO ensures *file_recovery==\old(*file_recovery); */
+// ensures (\result == 1) ==>  \separated(file_recovery_new, file_recovery_new->extension);
 static int header_check_bmp(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 bmp_header *bm=(const struct bmp_header *)buffer;

src/file_dir.c

@@ -66,6 +66,7 @@ static void file_rename_fatdir(file_recovery_t *file_recovery)
   fclose(file);
   if(buffer_size<32)
     return;
+  /*@ assert buffer_size >= 32; */
   cluster=fat_get_cluster_from_entry((const struct msdos_dir_entry *)&buffer[0]);
   sprintf(buffer_cluster, "cluster_%u", cluster);
   file_rename(file_recovery, buffer_cluster, strlen(buffer_cluster), 0, NULL, 1);
@@ -109,6 +110,7 @@ static int header_check_dir(const unsigned char *buffer, const unsigned int buff
   file_recovery_new->file_check=&file_check_size;
   file_recovery_new->file_rename=&file_rename_fatdir;
   file_recovery_new->time=date_dos2unix(le16(de->time),le16(de->date));
+  /*@ assert valid_file_recovery(file_recovery_new); */
   return 1;
 }
 

src/file_fits.c

@@ -118,7 +118,7 @@ static uint64_t fits_info(const unsigned char *buffer, const unsigned int buffer
       if(tmp > PHOTOREC_MAX_FILE_SIZE)
 	naxis_size=0;
       else if(tmp>0)
-      {
+      { /* FIXME overflow */
 	naxis_size*=(tmp+8-1)/8;
       }
     }
@@ -135,7 +135,7 @@ static uint64_t fits_info(const unsigned char *buffer, const unsigned int buffer
       if(naxis_val > PHOTOREC_MAX_FILE_SIZE)
 	naxis_size=0;
       else
-      {
+      { /* FIXME overflow */
 	naxis_size*=naxis_val;
       }
     }

src/file_found.h

@@ -25,6 +25,11 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(current_search_space);
+  @ requires \valid(file_stat);
+  @ requires \separated(current_search_space, file_stat);
+  @*/
 alloc_data_t *file_found(alloc_data_t *current_search_space, const uint64_t offset, file_stat_t *file_stat);
 
 #ifdef __cplusplus

src/file_gz.c

@@ -249,6 +249,7 @@ static int header_check_gz(const unsigned char *buffer, const unsigned int buffe
 #endif
     if(file_recovery->file_check==&file_check_bgzf)
     {
+      /*@ assert \valid_function(file_recovery->file_check); */
       header_ignored(file_recovery_new);
       return 0;
     }

src/file_list.c

@@ -371,7 +371,7 @@ extern const file_hint_t file_hint_zpr;
 
 file_enable_t array_file_enable[]=
 {
-#if (!defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_sig)) && !defined(__FRAMAC__)
+#if ((!defined(SINGLE_FORMAT)  && !defined(__FRAMAC__)) || defined(SINGLE_FORMAT_sig))
   { .enable=0, .file_hint=&file_hint_sig  },
 #endif
 #if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_1cd)

src/file_mlv.c

@@ -161,6 +161,7 @@ static void file_check_mlv(file_recovery_t *file_recovery)
 
 /*@
   @ requires valid_file_recovery(file_recovery);
+  @ requires file_recovery->file_rename == &file_rename_mlv;
   @*/
 static void file_rename_mlv(file_recovery_t *file_recovery)
 {

src/file_png.c

@@ -41,6 +41,7 @@
 
 extern const file_hint_t file_hint_doc;
 
+/*@ requires \valid(file_stat); */
 static void register_header_check_png(file_stat_t *file_stat);
 static data_check_t data_check_png(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
 static data_check_t data_check_mng(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);

src/file_template.c

@@ -31,6 +31,7 @@
 #include "types.h"
 #include "filegen.h"
 
+/*@ requires \valid(file_stat); */
 static void register_header_check_EXTENSION(file_stat_t *file_stat);
 
 const file_hint_t file_hint_EXTENSION= {

src/file_tiff.c

@@ -20,7 +20,7 @@
 
  */
 
-#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg) || defined(SINGLE_FORMAT_rw2) || defined(SINGLE_FORMAT_orf)
+#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg) || defined(SINGLE_FORMAT_rw2) || defined(SINGLE_FORMAT_orf) || defined(SINGLE_FORMAT_wdp)
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
@@ -185,7 +185,7 @@ static void register_header_check_tiff(file_stat_t *file_stat)
 {
   static const unsigned char tiff_header_be[4]= { 'M','M',0x00, 0x2a};
   static const unsigned char tiff_header_le[4]= { 'I','I',0x2a, 0x00};
-#if !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf)
+#if !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf) && !defined(SINGLE_FORMAT_wdp)
 #if !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
   register_header_check(0, tiff_header_be, sizeof(tiff_header_be), &header_check_tiff_be, file_stat);
 #endif

src/filegen.c

@@ -758,7 +758,7 @@ void header_ignored_cond_reset(uint64_t start, uint64_t end)
 /* 0: file_recovery_new->location.start has been taken into account, offset_skipped_header may have been updated
  * 1: file_recovery_new->location.start has been ignored */
 /*@
-  @ requires separation: \separated(file_recovery, file_recovery_new, &errno, &offset_skipped_header);
+  @ requires separation: \separated(file_recovery, file_recovery->handle, file_recovery_new, &errno, &offset_skipped_header);
   @*/
 int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery_t *file_recovery_new)
 {

src/filegen.h

@@ -319,7 +319,7 @@ void header_ignored_cond_reset(uint64_t start, uint64_t end);
 void header_ignored(const file_recovery_t *file_recovery_new);
 
 /*@
-  @ requires separation: \separated(file_recovery, file_recovery_new, &errno);
+  @ requires separation: \separated(file_recovery, file_recovery->handle, file_recovery_new, &errno);
   @ requires \valid_read(file_recovery);
   @ requires \valid_read(file_recovery_new);
   @ requires valid_file_recovery(file_recovery);
@@ -327,7 +327,6 @@ void header_ignored(const file_recovery_t *file_recovery_new);
   @ requires \valid_function(file_recovery->file_check);
   @ requires \initialized(&file_recovery->file_check);
   @ requires \initialized(&file_recovery->handle);
-  @ requires \separated(file_recovery, file_recovery->handle);
   @ ensures \result == 0 || \result == 1;
   @*/
 // ensures  valid_file_recovery(file_recovery);