Numerous frama-c annotations

src/alignio.h

@@ -26,13 +26,14 @@
 /*@
   @ requires \valid_function(fnct_pread);
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires disk_car->sector_size > 0;
   @ requires disk_car->offset < 0x8000000000000000;
   @ requires 0 < count < 0x8000000000000000;
   @ requires offset < 0x8000000000000000;
   @ requires \valid((char *)buf + (0 .. count -1));
-  @ requires disk_car->rbuffer == \null || (\freeable(disk_car->rbuffer) && disk_car->rbuffer_size > 0);
+  @ requires \separated(disk_car, (char *)buf);
-  @ ensures  disk_car->rbuffer == \null || (\freeable(disk_car->rbuffer) && disk_car->rbuffer_size > 0);
+  @ ensures  valid_disk(disk_car);
   @*/
 static int align_pread(int (*fnct_pread)(const disk_t *disk_car, void *buf, const unsigned int count, const uint64_t offset),
            disk_t *disk_car, void*buf, const unsigned int count, const uint64_t offset)
@@ -64,13 +65,17 @@ static int align_pread(int (*fnct_pread)(const disk_t *disk_car, void *buf, cons
       }
       /*@ assert disk_car->rbuffer_size >= count_new; */
       disk_car->rbuffer=(char*)MALLOC(disk_car->rbuffer_size);
+      /*@ assert valid_disk(disk_car); */
     }
     /*@ assert \freeable(disk_car->rbuffer); */
+    /*@ assert valid_disk(disk_car); */
     res=fnct_pread(disk_car, disk_car->rbuffer, count_new, offset_new/disk_car->sector_size*disk_car->sector_size);
     memcpy(buf,(char*)disk_car->rbuffer+(offset_new%disk_car->sector_size),count);
     /*@ assert \freeable(disk_car->rbuffer) && disk_car->rbuffer_size > 0; */
+    /*@ assert valid_disk(disk_car); */
     return (res < (signed)count ?  res : (signed)count );
   }
+  /*@ assert valid_disk(disk_car); */
   return fnct_pread(disk_car, buf, count, offset_new);
 }
 
@@ -78,13 +83,14 @@ static int align_pread(int (*fnct_pread)(const disk_t *disk_car, void *buf, cons
   @ requires \valid_function(fnct_pread);
   @ requires \valid_function(fnct_pwrite);
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires disk_car->sector_size > 0;
   @ requires disk_car->offset < 0x8000000000000000;
   @ requires 0 < count < 0x8000000000000000;
   @ requires offset < 0x8000000000000000;
   @ requires \valid_read((char *)buf + (0 .. count -1));
-  @ requires disk_car->wbuffer == \null || \freeable(disk_car->wbuffer);
+  @ requires \separated(disk_car, (char *)buf);
-  @ ensures  disk_car->wbuffer == \null || \freeable(disk_car->wbuffer);
+  @ ensures  valid_disk(disk_car);
   @*/
 static int align_pwrite(int (*fnct_pread)(const disk_t *disk_car, void *buf, const unsigned int count, const uint64_t offset),
     int (*fnct_pwrite)(disk_t *disk_car, const void *buf, const unsigned int count, const uint64_t offset),
@@ -113,8 +119,10 @@ static int align_pwrite(int (*fnct_pread)(const disk_t *disk_car, void *buf, con
       }
       /*@ assert disk_car->wbuffer_size >= count_new; */
       disk_car->wbuffer=(char*)MALLOC(disk_car->wbuffer_size);
+      /*@ assert valid_disk(disk_car); */
     }
     /*@ assert \freeable(disk_car->wbuffer); */
+    /*@ assert valid_disk(disk_car); */
     if(fnct_pread(disk_car, disk_car->wbuffer, count_new, offset_new/disk_car->sector_size*disk_car->sector_size)<0)
     {
       log_error("read failed but trying to write anyway");
@@ -123,8 +131,10 @@ static int align_pwrite(int (*fnct_pread)(const disk_t *disk_car, void *buf, con
     memcpy((char*)disk_car->wbuffer+(offset_new%disk_car->sector_size),buf,count);
     tmp=fnct_pwrite(disk_car, disk_car->wbuffer, count_new, offset_new/disk_car->sector_size*disk_car->sector_size);
     /*@ assert \freeable(disk_car->wbuffer) && disk_car->wbuffer_size > 0; */
+    /*@ assert valid_disk(disk_car); */
     return (tmp < (signed)count ? tmp : (signed)count);
   }
+  /*@ assert valid_disk(disk_car); */
   return fnct_pwrite(disk_car, buf, count, offset_new);
 }
 #endif

src/analyse.h

@@ -25,18 +25,121 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_type_0(const unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_type_1(const unsigned char *buffer, const disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_type_2(const unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_type_8(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_type_16(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_type_64(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_type_128(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_type_2048(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk, partition);
+  @*/
 int search_exFAT_backup(unsigned char *buffer, disk_t *disk, partition_t *partition);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_FAT_backup(unsigned char *buffer, disk_t *disk_car,partition_t *partition, const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_HFS_backup(unsigned char *buffer, disk_t *disk_car,partition_t *partition, const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(buffer, disk_car, partition);
+  @*/
 int search_NTFS_backup(unsigned char *buffer, disk_t *disk_car,partition_t *partition, const int verbose, const int dump_ind);
+
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(disk, partition);
+  @*/
 int check_linux(disk_t *disk, partition_t *partition, const int verbose);
 
 #ifdef __cplusplus

src/autoset.h

@@ -27,6 +27,7 @@ extern "C" {
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ assigns disk_car->unit;
   @*/
 void autoset_unit(disk_t *disk_car);

src/bfs.h

@@ -88,12 +88,14 @@ struct disk_super_block          /* super block as it is on disk */
 /*@
   @ requires \valid(disk_car);
   @ requires \valid(partition);
+  @ requires valid_disk(disk_car);
   @ requires separation: \separated(disk_car, partition);
   @*/
 int check_BeFS(disk_t *disk_car, partition_t *partition);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(beos_block);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, beos_block, partition);

src/bsd.h

@@ -171,6 +171,7 @@ struct disklabel {
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
   @*/
@@ -178,6 +179,7 @@ int check_BSD(disk_t *disk_car, partition_t *partition, const int verbose, const
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(bsd_header);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, bsd_header, partition);

src/btrfs.h

@@ -140,7 +140,20 @@ struct btrfs_super_block {
 	uint8_t sys_chunk_array[BTRFS_SYSTEM_CHUNK_ARRAY_SIZE];
 } __attribute__ ((gcc_struct, __packed__));
 
-int check_btrfs(disk_t *disk_car,partition_t *partition);
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
+int check_btrfs(disk_t *disk_car, partition_t *partition);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, sb, partition);
+  @*/
 int recover_btrfs(const disk_t *disk_car, const struct btrfs_super_block *sb,partition_t *partition,const int verbose, const int dump_ind);
 
 #ifdef __cplusplus

src/chgarch.h

@@ -27,9 +27,13 @@ extern "C" {
 #endif
 
 /*@
+  @ requires \valid(current_cmd);
   @ requires \valid(disk);
+  @ requires \separated(disk, current_cmd);
+  @ requires valid_disk(disk);
   @ requires current_cmd == \null || valid_read_string(*current_cmd);
   @ ensures  current_cmd == \null || valid_read_string(*current_cmd);
+  @ ensures  valid_disk(disk);
   @*/
 int change_arch_type_cli(disk_t *disk, const int verbose, char**current_cmd);
 

src/chgtype.h

@@ -25,6 +25,14 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid(current_cmd);
+  @ requires \separated(disk_car, partition, current_cmd);
+  @*/
 void change_part_type_cli(const disk_t *disk_car,partition_t *partition, char **current_cmd);
 
 #ifdef __cplusplus

src/chgtypen.h

@@ -25,6 +25,12 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid(partition);
+  @ requires \separated(disk, partition);
+  @*/
 void change_part_type_ncurses(const disk_t *disk, partition_t *partition);
 
 #ifdef __cplusplus

src/cramfs.h

@@ -84,7 +84,21 @@ struct cramfs_super {
 };
 
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 int check_cramfs(disk_t *disk_car,partition_t *partition,const int verbose);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition, sb);
+  @ requires \valid_read(sb);
+  @*/
 int recover_cramfs(const disk_t *disk_car, const struct cramfs_super *sb, partition_t *partition, const int verbose, const int dump_ind);
 
 #ifdef __cplusplus

src/dimage.h

@@ -25,6 +25,13 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_read_string(image_dd);
+  @ requires \separated(disk_car, partition, image_dd);
+  @*/
 int disk_image(disk_t *disk_car, const partition_t *partition, const char *image_dd);
 
 #ifdef __cplusplus

src/dir.c

@@ -57,8 +57,9 @@
 const char *monstr[] = { "Jan", "Feb", "Mar", "Apr", "May", "Jun",
 				"Jul", "Aug", "Sep", "Oct", "Nov", "Dec"};
 
-static char ftypelet (unsigned int bits);
+/*@
-
+  @ assigns \result;
+  @*/
 static char ftypelet (unsigned int bits)
 {
 #ifdef LINUX_S_ISBLK
@@ -195,6 +196,7 @@ int dir_aff_log(const dir_data_t *dir_data, const file_info_t *dir_list)
   {
     log_info("Directory %s\n",dir_data->current_directory);
   }
+#ifndef __FRAMAC__
   td_list_for_each(file_walker, &dir_list->list)
   {
     const file_info_t *current_file=td_list_entry_const(file_walker, const file_info_t, list);
@@ -222,11 +224,13 @@ int dir_aff_log(const dir_data_t *dir_data, const file_info_t *dir_list)
     }
     log_info("%s\n", current_file->name);
   }
+#endif
   return test_date;
 }
 
 void log_list_file(const disk_t *disk, const partition_t *partition, const dir_data_t *dir_data, const file_info_t*list)
 {
+#ifndef __FRAMAC__
   struct td_list_head *tmp;
   log_partition(disk, partition);
   if(dir_data!=NULL)
@@ -250,6 +254,7 @@ void log_list_file(const disk_t *disk, const partition_t *partition, const dir_d
     log_info("%9llu", (long long unsigned int)current_file->st_size);
     log_info(" %s %s\n", datestr, current_file->name);
   }
+#endif
 }
 
 unsigned int delete_list_file(file_info_t *file_info)
@@ -269,6 +274,11 @@ unsigned int delete_list_file(file_info_t *file_info)
   return nbr;
 }
 
+/*@
+  @ requires \valid_read(current_file);
+  @ requires \valid_read(inode_known + (0 .. dir_nbr-1));
+  @ assigns \nothing;
+  @*/
 static int is_inode_valid(const file_info_t *current_file, const unsigned int dir_nbr, const unsigned long int *inode_known)
 {
   const unsigned long int new_inode=current_file->st_ino;
@@ -277,12 +287,21 @@ static int is_inode_valid(const file_info_t *current_file, const unsigned int di
     return 0;
   if(strcmp(current_file->name, "..")==0)
     return 0;
+  /*@ loop assigns i; */
   for(i=0; i<dir_nbr; i++)
     if(new_inode==inode_known[i]) /* Avoid loop */
       return 0;
   return 1;
 }
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid(dir_data);
+  @ requires \separated(disk, partition, dir_data);
+  @*/
 static int dir_whole_partition_log_aux(disk_t *disk, const partition_t *partition, dir_data_t *dir_data, const unsigned long int inode)
 {
   struct td_list_head *file_walker = NULL;
@@ -325,6 +344,16 @@ int dir_whole_partition_log(disk_t *disk, const partition_t *partition, dir_data
   return dir_whole_partition_log_aux(disk, partition, dir_data, inode);
 }
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid(dir_data);
+  @ requires \valid(copy_ok);
+  @ requires \valid(copy_bad);
+  @ requires \separated(disk, partition, dir_data, copy_ok, copy_bad);
+  @*/
 static int dir_whole_partition_copy_aux(disk_t *disk, const partition_t *partition, dir_data_t *dir_data, const unsigned long int inode, unsigned int *copy_ok, unsigned int *copy_bad)
 {
   struct td_list_head *file_walker = NULL;
@@ -450,11 +479,14 @@ static struct {
   { 0, 0 }
 };
 
+/*@
+  @ assigns \nothing;
+  @*/
 static mode_t mode_xlate(unsigned int lmode)
 {
   mode_t  mode = 0;
   int     i;
-
+  /*@ loop assigns i, mode; */
   for (i=0; mode_table[i].lmask; i++) {
     if (lmode & mode_table[i].lmask)
       mode |= mode_table[i].mask;
@@ -481,6 +513,9 @@ int set_mode(const char *pathname, unsigned int mode)
 #endif
 }
 
+/*@
+  @ requires valid_string(fn);
+  @*/
 static void strip_fn(char *fn)
 {
   unsigned int i;
@@ -642,9 +677,17 @@ static unsigned int filename_convert(char *dst, const char*src, const unsigned i
   return j;
 }
 #else
+/*@
+  @ requires \valid(dst + (0 .. n));
+  @ requires \valid_read(src + (0 .. n-1));
+  @ requires \separated(dst + (..), src + (..));
+  @*/
 static unsigned int filename_convert(char *dst, const char*src, const unsigned int n)
 {
   unsigned int i;
+  /*@
+    @ loop assigns i, dst[i];
+    @*/
   for(i=0;i<n && src[i]!='\0';i++)
     dst[i]=src[i];
   dst[i]='\0';

src/dir.h

@@ -32,21 +32,84 @@ extern "C" {
 int set_datestr(char *datestr, size_t n, const time_t timev);
 
 /*@
-  @ requires \valid_read(dir_data);
+  @ requires dir_data==\null || \valid_read(dir_data);
   @ requires \valid_read(dir_list);
+  @ requires \separated(dir_data, dir_list);
   @*/
 int dir_aff_log(const dir_data_t *dir_data, const file_info_t*dir_list);
 
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid_read(dir_data);
+  @ requires \valid_read(list);
+  @*/
 void log_list_file(const disk_t *disk_car, const partition_t *partition, const dir_data_t *dir_data, const file_info_t*list);
+
+/*@
+  @ requires \valid(list);
+  @*/
 unsigned int delete_list_file(file_info_t *list);
+
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid_read(dir_data);
+  @ requires \separated(disk_car, partition, dir_data);
+  @*/
 int dir_whole_partition_log(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const unsigned long int inode);
+
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid_read(dir_data);
+  @ requires \separated(disk_car, partition, dir_data);
+  @*/
 void dir_whole_partition_copy(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const unsigned long int inode);
+
+/*@
+  @ requires \valid(str + (0 .. 9));
+  @ assigns str[0 .. 9];
+  @*/
 void mode_string (const unsigned int mode, char *str);
+
+/*@
+  @ requires valid_read_string(pathname);
+  @*/
 int set_mode(const char *pathname, unsigned int mode);
+
+/*@
+  @ requires valid_read_string(filename);
+  @ requires \separated(localfilename, localroot, filename);
+  @*/
 FILE *fopen_local(char **localfilename, const char *localroot, const char *filename);
+
+/*@
+  @ requires valid_read_string(filename);
+  @*/
 char *gen_local_filename(const char *filename);
+
+/*@
+  @ requires valid_read_string(localroot);
+  @ requires valid_read_string(pathname);
+  @*/
 char *mkdir_local(const char *localroot, const char *pathname);
+
+/*@
+  @ requires valid_read_string(filename);
+  @*/
 void mkdir_local_for_file(const char *filename);
+
+/*@
+  @ requires \valid_read(a);
+  @ requires \valid_read(b);
+  @*/
 int filesort(const struct td_list_head *a, const struct td_list_head *b);
 #ifdef __cplusplus
 } /* closing brace for extern "C" */

src/dirn.h

@@ -25,6 +25,12 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires \separated(disk_car, partition, dir_data, current_cmd);
+  @*/
 int dir_partition_aff(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const unsigned long int inode, char **current_cmd);
 
 #ifdef __cplusplus

src/dirpart.h

@@ -26,6 +26,12 @@ extern "C" {
 #endif
 
 #include "dir.h"
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires \separated(disk_car, partition, current_cmd);
+  @*/
 dir_partition_t dir_partition(disk_t *disk_car, const partition_t *partition, const int verbose, const int expert, char **current_cmd);
 
 #ifdef __cplusplus

src/diskacc.h

@@ -25,6 +25,11 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \separated(disk_car, current_cmd);
+  @*/
 int interface_check_disk_access(disk_t *disk_car, char **current_cmd);
 
 #ifdef __cplusplus

src/diskcapa.h

@@ -25,6 +25,10 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 int interface_check_disk_capacity(disk_t *disk_car);
 
 #ifdef __cplusplus

src/edit.h

@@ -25,6 +25,10 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 void interface_editor(disk_t *disk_car);
 
 #ifdef __cplusplus

src/ewf.h

@@ -30,8 +30,13 @@ extern "C" {
 #endif
 
 #if defined(HAVE_LIBEWF_H) && defined(HAVE_LIBEWF)
+/*@
+  @ requires valid_read_string(device);
+  @ ensures  valid_disk(\result);
+  @*/
 disk_t *fewf_init(const char *device, const int testdisk_mode);
 #endif
+/*@ assigns \nothing; */
 const char*td_ewf_version(void);
 
 #ifdef __cplusplus

src/exfat.c

@@ -50,6 +50,11 @@ int exfat_read_cluster(disk_t *disk, const partition_t *partition, const struct
       partition->part_offset + exfat_cluster_to_offset(exfat_header, cluster));
 }
 
+/*@
+  @ requires \valid(partition);
+  @ requires \valid_read(exfat_header);
+  @ requires \separated(partition, exfat_header);
+  @*/
 static void set_exFAT_info(partition_t *partition, const struct exfat_super_block*exfat_header)
 {
   partition->upart_type=UP_EXFAT;

src/exfat.h

@@ -94,10 +94,42 @@ struct exfat_alloc_bitmap_entry
   uint64_t data_length;
 } __attribute__ ((gcc_struct, __packed__));
 
+/*@
+  @ requires \valid_read(exfat_header);
+  @ assigns \nothing;
+  @*/
 uint64_t exfat_cluster_to_offset(const struct exfat_super_block *exfat_header, const unsigned int cluster);
+
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(partition);
+  @ requires \valid_read(exfat_header);
+  @ requires \separated(disk, partition, exfat_header, (char *)buffer);
+  @*/
 int exfat_read_cluster(disk_t *disk, const partition_t *partition, const struct exfat_super_block*exfat_header, void *buffer, const unsigned int cluster);
+
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid(partition);
+  @ requires \separated(disk, partition);
+  @*/
 int check_exFAT(disk_t *disk, partition_t *partition);
+
+/*@
+  @ requires \valid_read(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(disk, exfat_header, partition);
+  @*/
 int recover_exFAT(const disk_t *disk, const struct exfat_super_block *exfat_header, partition_t *partition);
+
+/*@
+  @ requires \valid_read(exfat_header);
+  @ assigns \nothing;
+  @*/
 int test_exFAT(const struct exfat_super_block *exfat_header);
 
 #ifdef __cplusplus

src/exfat_dir.h

@@ -25,6 +25,12 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires \separated(disk_car, partition, dir_data);
+  @*/
 dir_partition_t dir_partition_exfat_init(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const int verbose);
 
 #ifdef __cplusplus

src/exfatp.c

@@ -37,9 +37,14 @@
 #include "log.h"
 #include "fat.h"
 
+/*@
+  @ requires \valid_read(buffer + ( 0 .. size-1));
+  @ assigns \nothing;
+  @*/
 static struct exfat_alloc_bitmap_entry *exfat_get_bitmap(unsigned char*buffer, const unsigned int size)
 {
   unsigned int i;
+  /*@ loop assigns i; */
   for(i=0; i<size; i+=0x20)
     if(buffer[i]==0x81)
       return (struct exfat_alloc_bitmap_entry *)&buffer[i];

src/exfatp.h

@@ -25,6 +25,15 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires valid_list_search_space(list_search_space);
+  @ requires \separated(disk, partition, list_search_space);
+  @*/
+// ensures  valid_list_search_space(list_search_space);
 unsigned int exfat_remove_used_space(disk_t *disk, const partition_t *partition, alloc_data_t *list_search_space);
 
 #ifdef __cplusplus

src/ext2_common.h

@@ -218,6 +218,7 @@ uint64_t td_ext2fs_free_blocks_count(const struct ext2_super_block *super);
 
 /*@
   @ requires \valid_read(sb);
+  @ requires \initialized(sb);
   @ requires partition==\null || (\valid_read(partition) && valid_partition(partition));
   @ requires \separated(sb, partition);
   @ assigns  \nothing;

src/f2fs.h

@@ -25,8 +25,26 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid(partition);
+  @ requires \separated(disk, partition);
+  @*/
 int check_f2fs(disk_t *disk, partition_t *partition);
+
+/*@
+  @ requires \valid_read(hdr);
+  @*/
 int test_f2fs(const struct f2fs_super_block *hdr);
+
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(hdr);
+  @ requires \valid(partition);
+  @ requires \separated(disk, hdr, partition);
+  @*/
 int recover_f2fs(const disk_t *disk, const struct f2fs_super_block *hdr, partition_t *partition);
 
 #ifdef __cplusplus

src/fat.c

@@ -70,6 +70,14 @@ static int is_fat16(const partition_t *partition);
   @*/
 static int is_fat32(const partition_t *partition);
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid_read(fat_header);
+  @ requires \separated(disk_car, partition, fat_header);
+  @*/
 static int fat32_set_part_name(disk_t *disk_car, partition_t *partition, const struct fat_boot_sector*fat_header)
 {
   partition->fsname[0]='\0';
@@ -112,6 +120,12 @@ static int fat32_set_part_name(disk_t *disk_car, partition_t *partition, const s
   return 0;
 }
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires \valid_read(fat_header);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, fat_header, partition);
+  @*/
 static void set_FAT_info(disk_t *disk_car, const struct fat_boot_sector *fat_header, partition_t *partition)
 {
   uint64_t start_fat1;
@@ -160,6 +174,9 @@ static void set_FAT_info(disk_t *disk_car, const struct fat_boot_sector *fat_hea
   }
 }
 
+/*@
+  @ requires \valid_read(fh1);
+  @*/
 static int log_fat_info(const struct fat_boot_sector*fh1, const upart_type_t upart_type, const unsigned int sector_size)
 {
   log_info("sector_size  %u\n", fat_sector_size(fh1));
@@ -280,6 +297,13 @@ int check_FAT(disk_t *disk_car, partition_t *partition, const int verbose)
   return 0;
 }
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(disk, partition);
+  @*/
 static unsigned int get_next_cluster_fat12(disk_t *disk, const partition_t *partition, const int offset, const unsigned int cluster)
 {
   unsigned int next_cluster;
@@ -303,6 +327,13 @@ static unsigned int get_next_cluster_fat12(disk_t *disk, const partition_t *part
   return next_cluster;
 }
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(disk, partition);
+  @*/
 static unsigned int get_next_cluster_fat16(disk_t *disk, const partition_t *partition, const int offset, const unsigned int cluster)
 {
   unsigned int next_cluster;
@@ -324,6 +355,13 @@ static unsigned int get_next_cluster_fat16(disk_t *disk, const partition_t *part
   return next_cluster;
 }
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(disk, partition);
+  @*/
 static unsigned int get_next_cluster_fat32(disk_t *disk, const partition_t *partition, const int offset, const unsigned int cluster)
 {
   unsigned int next_cluster;
@@ -818,6 +856,13 @@ unsigned long int fat32_get_next_free(const unsigned char *boot_fat32, const uns
   return le32(fsinfo->nextfree);
 }
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(disk, partition);
+  @*/
 static int fat_has_EFI_entry(disk_t *disk, const partition_t *partition, const int verbose)
 {
   dir_data_t dir_data;
@@ -920,6 +965,34 @@ int recover_FAT(disk_t *disk_car, const struct fat_boot_sector*fat_header, parti
   return 0;
 }
 
+/*@
+  @ requires \valid_read(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(fat_header);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @*/
+static int test_OS2MB(const disk_t *disk, const struct fat_boot_sector *fat_header, const partition_t *partition, const int verbose, const int dump_ind)
+{
+  const char*buffer=(const char*)fat_header;
+  if(le16(fat_header->marker)==0xAA55 && memcmp(buffer+FAT_NAME1,"FAT     ",8)==0)
+  {
+#ifndef __FRAMAC__
+    if(verbose||dump_ind)
+    {
+      log_info("OS2MB at %u/%u/%u\n",
+	  offset2cylinder(disk, partition->part_offset),
+	  offset2head(disk, partition->part_offset),
+	  offset2sector(disk, partition->part_offset));
+    }
+#endif
+    if(dump_ind)
+      dump_log(buffer, DEFAULT_SECTOR_SIZE);
+    return 0;
+  }
+  return 1;
+}
+
 int check_OS2MB(disk_t *disk, partition_t *partition, const int verbose)
 {
   unsigned char *buffer=(unsigned char *)MALLOC(disk->sector_size);
@@ -958,25 +1031,6 @@ int recover_OS2MB(const disk_t *disk, const struct fat_boot_sector*fat_header, p
   return 0;
 }
 
-static int test_OS2MB(const disk_t *disk, const struct fat_boot_sector *fat_header, const partition_t *partition, const int verbose, const int dump_ind)
-{
-  const char*buffer=(const char*)fat_header;
-  if(le16(fat_header->marker)==0xAA55 && memcmp(buffer+FAT_NAME1,"FAT     ",8)==0)
-  {
-    if(verbose||dump_ind)
-    {
-      log_info("OS2MB at %u/%u/%u\n",
-	  offset2cylinder(disk, partition->part_offset),
-	  offset2head(disk, partition->part_offset),
-	  offset2sector(disk, partition->part_offset));
-    }
-    if(dump_ind)
-      dump_log(buffer, DEFAULT_SECTOR_SIZE);
-    return 0;
-  }
-  return 1;
-}
-
 int is_fat(const partition_t *partition)
 {
   return (is_fat12(partition)||is_fat16(partition)||is_fat32(partition));
@@ -1124,6 +1178,9 @@ int fat32_free_info(disk_t *disk_car,const partition_t *partition, const unsigne
 int check_VFAT_volume_name(const char *name, const unsigned int max_size)
 {
   unsigned int i;
+  /*@
+    @ loop assigns i;
+    @*/
   for(i=0; i<max_size && name[i]!='\0'; i++)
   {
     if(name[i] < 0x20)

src/fat.h

@@ -29,7 +29,9 @@ extern "C" {
 #include "fat_common.h"
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
   @*/
 int comp_FAT(disk_t *disk, const partition_t *partition, const unsigned long int fat_size, const unsigned long int sect_res);
@@ -42,14 +44,18 @@ int log_fat2_info(const struct fat_boot_sector*fh1, const struct fat_boot_sector
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
   @*/
 unsigned int get_next_cluster(disk_t *disk, const partition_t *partition, const upart_type_t upart_type, const int offset, const unsigned int cluster);
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
   @*/
 int set_next_cluster(disk_t *disk, const partition_t *partition, const upart_type_t upart_type, const int offset, const unsigned int cluster, const unsigned int next_cluster);
@@ -86,14 +92,18 @@ int is_part_fat32(const partition_t *partition);
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
   @*/
 unsigned int fat32_get_prev_cluster(disk_t *disk, const partition_t *partition, const unsigned int fat_offset, const unsigned int cluster, const unsigned int no_of_cluster);
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
   @ requires \valid(next_free);
   @ requires \valid(free_count);
@@ -114,44 +124,55 @@ unsigned long int fat32_get_next_free(const unsigned char *boot_fat32, const uns
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid_read(fat_header);
   @ requires \valid(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition, fat_header);
   @*/
 int recover_FAT(disk_t *disk, const struct fat_boot_sector*fat_header, partition_t *partition, const int verbose, const int dump_ind, const int backup);
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
   @*/
 int check_FAT(disk_t *disk, partition_t *partition, const int verbose);
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid_read(fat_header);
   @ requires \valid(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition, fat_header);
   @*/
 int test_FAT(disk_t *disk, const struct fat_boot_sector *fat_header, const partition_t *partition, const int verbose, const int dump_ind);
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid_read(fat_header);
   @ requires \valid(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition, fat_header);
   @*/
 int recover_OS2MB(const disk_t *disk, const struct fat_boot_sector*fat_header, partition_t *partition, const int verbose, const int dump_ind);
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
   @*/
 int check_OS2MB(disk_t *disk, partition_t *partition, const int verbose);
 
 /*@
   @ requires \valid_read(name);
+  @ assigns \nothing;
   @*/
 int check_VFAT_volume_name(const char *name, const unsigned int max_size);
 

src/fat1x.h

@@ -25,6 +25,12 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 int fat1x_boot_sector(disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind, const unsigned int expert, char **current_cmd);
 
 #ifdef __cplusplus

src/fat32.h

@@ -25,6 +25,12 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 int fat32_boot_sector(disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind, const unsigned int expert, char **current_cmd);
 
 #ifdef __cplusplus

src/fat_adv.h

@@ -25,8 +25,28 @@
 extern "C" {
 #endif
 
-int rebuild_FAT_BS(disk_t *disk_car,partition_t *partition, const int verbose, const int dump_ind, const unsigned int expert, char**current_cmd);
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
+int rebuild_FAT_BS(disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind, const unsigned int expert, char**current_cmd);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 int FAT_init_rootdir(disk_t *disk_car, partition_t *partition, const int verbose, char **current_cmd);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 int repair_FAT_table(disk_t *disk_car, partition_t *partition, const int verbose, char **current_cmd);
 
 #ifdef __cplusplus

src/fat_cluster.h

@@ -42,9 +42,29 @@ struct cluster_offset_struct
   unsigned int  first_sol;
 };
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid(sectors_per_cluster);
+  @ requires \valid(offset);
+  @ requires \separated(disk_car, partition, sectors_per_cluster, offset);
+  @*/
 int find_sectors_per_cluster(disk_t *disk_car, const partition_t *partition, const int verbose, const int dump_ind, unsigned int *sectors_per_cluster, uint64_t *offset, const upart_type_t upart_type);
+
+/*@
+  @ assigns \nothing;
+  @*/
 upart_type_t no_of_cluster2part_type(const unsigned long int no_of_cluster);
-int find_sectors_per_cluster_aux(const sector_cluster_t *sector_cluster, const unsigned int nbr_sector_cluster,unsigned int *sectors_per_cluster, uint64_t *offset, const int verbose, const unsigned long int part_size_in_sectors, const upart_type_t upart_type);
+
+/*@
+  @ requires \valid_read(sector_cluster + (0 .. nbr_sector_cluster-1));
+  @ requires \valid(sectors_per_cluster);
+  @ requires \valid(offset);
+  @ requires \separated(sector_cluster + (..), sectors_per_cluster, offset);
+  @*/
+int find_sectors_per_cluster_aux(const sector_cluster_t *sector_cluster, const unsigned int nbr_sector_cluster, unsigned int *sectors_per_cluster, uint64_t *offset, const int verbose, const unsigned long int part_size_in_sectors, const upart_type_t upart_type);
 
 #ifdef __cplusplus
 } /* closing brace for extern "c" */

src/fat_dir.c

@@ -55,14 +55,42 @@ struct fat_dir_struct
   struct fat_boot_sector*boot_sector;
 };
 
-
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid_read(dir_data);
+  @ requires \valid_read(fat_header);
+  @ requires \valid(dir_list);
+  @ requires \separated(disk_car, partition, dir_data, fat_header, dir_list);
+  @*/
 static int fat1x_rootdir(disk_t *disk_car, const partition_t *partition, const dir_data_t *dir_data, const struct fat_boot_sector*fat_header, file_info_t *dir_list);
-static inline void fat16_towchar(wchar_t *dst, const uint8_t *src, size_t len);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid_read(dir_data);
+  @ requires \valid(file);
+  @ requires \separated(disk_car, partition, dir_data, file);
+  @*/
 static int fat_copy(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const file_info_t *file);
+
+/*@
+  @ requires \valid(dir_data);
+  @*/
 static void dir_partition_fat_close(dir_data_t *dir_data);
 
+/*@
+  @ requires len > 0;
+  @ requires \valid_read(src + (0 .. 2*len-1));
+  @ requires \valid((char *)dst + (0 .. 2*len-1));
+  @*/
 static inline void fat16_towchar(wchar_t *dst, const uint8_t *src, size_t len)
 {
+	/*@ loop assigns len, *dst, dst, src; */
 	while (len--) {
 		*dst++ = src[0] | (src[1] << 8);
 		src += 2;
@@ -271,16 +299,16 @@ RecEnd:
 #endif
 	  if(sizec <= 0)
 	  {
-	    new_file->name[o++]=(char) unicode[i];
+	    new_file->name[o++]=unicode[i];
 	    utf8=0;
 	  }
 	  else
 	    o += sizec;
 	}
 	else
-	  new_file->name[o++]=(char) unicode[i];
+	  new_file->name[o++]=unicode[i];
       }
-      new_file->name[o]=0;
+      new_file->name[o]='\0';
       new_file->st_ino=inode;
       new_file->st_mode = MSDOS_MKMODE(de->attr,(LINUX_S_IRWXUGO & ~(LINUX_S_IWGRP|LINUX_S_IWOTH)));
       new_file->st_uid=0;
@@ -302,6 +330,7 @@ RecEnd:
 
 typedef enum {FAT_FOLLOW_CLUSTER, FAT_NEXT_FREE_CLUSTER, FAT_NEXT_CLUSTER} fat_method_t;
 
+/*@ assigns \nothing; */
 static int is_EOC(const unsigned int cluster, const upart_type_t upart_type)
 {
   if(upart_type==UP_FAT12)
@@ -313,6 +342,16 @@ static int is_EOC(const unsigned int cluster, const upart_type_t upart_type)
 }
 
 #define NBR_ENTRIES_MAX 65536
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid_read(dir_data);
+  @ requires \valid(dir_list);
+  @ requires \separated(disk_car, partition, dir_data, dir_list);
+  @*/
 static int fat_dir(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const unsigned long int first_cluster, file_info_t *dir_list)
 {
   const struct fat_dir_struct *ls=(const struct fat_dir_struct*)dir_data->private_dir_data;
@@ -482,6 +521,15 @@ static void dir_partition_fat_close(dir_data_t *dir_data)
   free(ls);
 }
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid(dir_data);
+  @ requires \valid_read(file);
+  @ requires \separated(disk_car, partition, dir_data, file);
+  @*/
 static int fat_copy(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const file_info_t *file)
 {
   char *new_file;	

src/fat_dir.h

@@ -26,7 +26,22 @@ extern "C" {
 #endif
 #include "dir_common.h"
 
+/*@
+  @ requires \valid_read(buffer + (0 .. size-1));
+  @ requires \initialized(buffer + (0 .. size-1));
+  @ requires \valid(dir_list);
+  @ requires \separated(dir_list, buffer+(..));
+  @*/
 int dir_fat_aux(const unsigned char*buffer, const unsigned int size, const unsigned int param, file_info_t *dir_list);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid(dir_data);
+  @ requires \separated(disk_car, partition, dir_data);
+  @*/
 dir_partition_t dir_partition_fat_init(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const int verbose);
 
 #ifdef __cplusplus

src/fatp.c

@@ -37,6 +37,14 @@
 #include "fat_common.h"
 #include "log.h"
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid(list_search_space);
+  @ requires \separated(disk, partition, list_search_space);
+  @*/
 static void fat12_remove_used_space(disk_t *disk,const partition_t *partition, alloc_data_t *list_search_space, const unsigned int fat_offset, const unsigned int no_of_cluster, const unsigned int start_data, const unsigned int cluster_size, const unsigned int sector_size)
 {
   unsigned char *buffer;
@@ -86,6 +94,14 @@ static void fat12_remove_used_space(disk_t *disk,const partition_t *partition, a
     del_search_space(list_search_space, start_free, end_free);
 }
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid(list_search_space);
+  @ requires \separated(disk_car, partition, list_search_space);
+  @*/
 static void fat16_remove_used_space(disk_t *disk_car,const partition_t *partition, alloc_data_t *list_search_space, const unsigned int fat_offset, const unsigned int no_of_cluster, const unsigned int start_data, const unsigned int cluster_size, const unsigned int sector_size)
 {
   unsigned char *buffer;
@@ -130,6 +146,14 @@ static void fat16_remove_used_space(disk_t *disk_car,const partition_t *partitio
     del_search_space(list_search_space, start_free, end_free);
 }
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid(list_search_space);
+  @ requires \separated(disk_car, partition, list_search_space);
+  @*/
 static void fat32_remove_used_space(disk_t *disk_car,const partition_t *partition, alloc_data_t *list_search_space, const unsigned int fat_offset, const unsigned int no_of_cluster, const unsigned int start_data, const unsigned int cluster_size, const unsigned int sector_size)
 {
   unsigned char *buffer;

src/fatp.h

@@ -25,6 +25,15 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires valid_list_search_space(list_search_space);
+  @ requires \separated(disk_car, partition, list_search_space);
+  @*/
+// ensures  valid_list_search_space(list_search_space);
 unsigned int fat_remove_used_space(disk_t *disk_car,const partition_t *partition, alloc_data_t *list_search_space);
 
 #ifdef __cplusplus

src/fatx.h

@@ -34,7 +34,19 @@ struct disk_fatx
   uint32_t	unknown;
 } __attribute__ ((gcc_struct, __packed__));
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 int check_FATX(disk_t *disk_car, partition_t *partition);
+
+/*@
+  @ requires \valid_read(fatx_block);
+  @ requires \valid(partition);
+  @ requires \separated(fatx_block, partition);
+  @*/
 int recover_FATX(const struct disk_fatx *fatx_block, partition_t *partition);
 
 #ifdef __cplusplus

src/fidentify.c

@@ -201,6 +201,7 @@ static int file_identify(const char *filename, const unsigned int options)
 	    (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)
 	  {
+	    /*@ assert valid_file_check_node(file_check); */
 	    /*@ assert valid_file_recovery(&file_recovery_new); */
 	    file_recovery_new.file_stat=file_check->file_stat;
 	    break;

src/file_txt.c

@@ -493,6 +493,7 @@ static double is_random(const unsigned char *buffer, const unsigned int buffer_s
     @ loop invariant \forall integer j; (0 <= j < i) ==> stats[j] == 0;
     @ loop invariant \initialized(&stats[0 .. i-1]);
     @ loop assigns i, stats[0 ..i];
+    @ loop variant 256-i;
     @ */
   for(i=0; i < 256; i++)
     stats[i] = 0;

src/filegen.c

@@ -147,13 +147,24 @@ void register_header_check(const unsigned int offset, const void *value, const u
   file_check_new->offset=offset;
   file_check_new->header_check=header_check;
   file_check_new->file_stat=file_stat;
+
+  /*@ assert \valid_read(file_check_new); */
+  /*@ assert \initialized(&file_check_new->offset); */
+  /*@ assert \initialized(&file_check_new->length); */
+  /*@ assert file_check_new->offset <= PHOTOREC_MAX_SIG_OFFSET; */
+  /*@ assert 0 < file_check_new->length <= PHOTOREC_MAX_SIG_SIZE; */
+  /*@ assert file_check_new->offset + file_check_new->length <= PHOTOREC_MAX_SIG_OFFSET; */
+  /*@ assert \valid_read((const char *)file_check_new->value+(0..file_check_new->length-1)); */
+  /*@ assert \valid_function(file_check_new->header_check); */
+  /*@ assert \valid(file_check_new->file_stat); */
+
+  /*@ assert valid_file_check_node(file_check_new); */
   td_list_add_sorted(&file_check_new->list, &file_check_plist.list, file_check_cmp);
 }
 
 /*@
   @ requires \valid(file_check_new);
-  @ requires initialization: \initialized(&file_check_new->offset) && \initialized(&file_check_new->length);
+  @ requires valid_file_check_node(file_check_new);
-  @ requires \valid_function(file_check_new->header_check);
   @*/
 static void index_header_check_aux(file_check_t *file_check_new)
 {
@@ -194,6 +205,7 @@ static unsigned int index_header_check(void)
   {
     file_check_t *current_check;
     current_check=td_list_entry(tmp, file_check_t, list);
+    /*@ assert valid_file_check_node(current_check); */
     /* dettach current_check from file_check_plist */
     td_list_del(tmp);
     /*@ assert \initialized(&current_check->offset) && \initialized(&current_check->length); */
@@ -228,6 +240,7 @@ void free_header_check(void)
 #endif
 	file_check_t *current_check;
 	current_check=td_list_entry(tmp, file_check_t, list);
+	/*@ assert valid_file_check_node(current_check); */
 #ifdef DEBUG_HEADER_CHECK
 	data=(const char *)current_check->value;
 	log_info("[%u]=%02x length=%u offset=%u", pos->offset, i, current_check->length, current_check->offset);

src/filegen.h

@@ -93,8 +93,7 @@ struct file_recovery_struct
   uint64_t extra;	/* extra bytes between offset_ok and offset_error */
   uint64_t calculated_file_size;
   data_check_t (*data_check)(const unsigned char*buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
-  /* data_check modifies file_recovery->calculated_file_size, it can also update data_check, file_check, offset_error, offset_ok, time */
+  /* data_check modifies file_recovery->calculated_file_size, it can also update data_check, file_check, offset_error, offset_ok, time, data_check_tmp */
-  /* side effect for data_check_flv */
   void (*file_check)(file_recovery_t *file_recovery);
   void (*file_rename)(file_recovery_t *file_recovery);
   uint64_t checkpoint_offset;
@@ -115,6 +114,19 @@ typedef struct
   file_stat_t *file_stat;
 } file_check_t;
 
+/*@
+   predicate valid_file_check_node(file_check_t *node) = (\valid_read(node) &&
+     \initialized(&node->offset) &&
+     \initialized(&node->length) &&
+     node->offset <= PHOTOREC_MAX_SIG_OFFSET &&
+     0 < node->length <= PHOTOREC_MAX_SIG_SIZE &&
+     node->offset + node->length <= PHOTOREC_MAX_SIG_OFFSET &&
+     \valid_read((const char *)node->value+(0..node->length-1)) &&
+     \valid_function(node->header_check) &&
+     \valid(node->file_stat)
+   );
+   @*/
+
 typedef struct
 {
   file_check_t file_checks[256];
@@ -335,6 +347,7 @@ void reset_file_recovery(file_recovery_t *file_recovery);
   @ requires \valid_read((const char *)value+(0..length-1));
   @ requires \valid_function(header_check);
   @ requires \valid(file_stat);
+  @ ensures  \valid_read((const char *)value+(0..length-1));
   @*/
 void register_header_check(const unsigned int offset, const void *value, const unsigned int length,
     int (*header_check)(const unsigned char *buffer, const unsigned int buffer_size,

src/geometry.c

@@ -79,7 +79,9 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
   int geo_modified=0;
   if(*current_cmd==NULL)
     return 0;
+#ifndef __FRAMAC__
   log_info("Current geometry\n%s sector_size=%u\n", disk_car->description(disk_car), disk_car->sector_size);
+#endif
   /*@ loop invariant valid_read_string(*current_cmd); */
   while (done==0)
   {
@@ -94,8 +96,10 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
 	if(geo_modified==0)
 	  geo_modified=1;
       }
+#ifndef __FRAMAC__
       else
 	log_error("Illegal cylinders value\n");
+#endif
     }
     else if(check_command(current_cmd,"H,",2)==0)
     {
@@ -108,8 +112,10 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
 	if(cyl_modified==0)
 	  set_cylinders_from_size_up(disk_car);
       }
+#ifndef __FRAMAC__
       else
 	log_error("Illegal heads value\n");
+#endif
     }
     else if(check_command(current_cmd,"S,",2)==0)
     {
@@ -121,16 +127,21 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
 	  geo_modified=1;
 	if(cyl_modified==0)
 	  set_cylinders_from_size_up(disk_car);
-      } else
+      }
+#ifndef __FRAMAC__
+      else
 	log_error("Illegal sectors value\n");
+#endif
     }
     else if(check_command(current_cmd,"N,",2)==0)
     {
       tmp_val = get_int_from_command(current_cmd);
-      if(change_sector_size(disk_car, cyl_modified, tmp_val))
+      if(change_sector_size(disk_car, cyl_modified, tmp_val)==0)
-	  log_error("Illegal sector size\n");
-      else
 	geo_modified=2;
+#ifndef __FRAMAC__
+      else
+	  log_error("Illegal sector size\n");
+#endif
     }
     else
     {
@@ -139,6 +150,7 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
     if(cyl_modified!=0)
       disk_car->disk_size=(uint64_t)disk_car->geom.cylinders*disk_car->geom.heads_per_cylinder*disk_car->geom.sectors_per_head*disk_car->sector_size;
   }
+  /*@ assert valid_read_string(*current_cmd); */
   if(geo_modified!=0)
   {
     disk_car->disk_size=(uint64_t)disk_car->geom.cylinders*disk_car->geom.heads_per_cylinder*disk_car->geom.sectors_per_head*disk_car->sector_size;
@@ -146,12 +158,16 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
     /* On MacOSX if HD contains some bad sectors, the disk size may not be correctly detected */
     disk_car->disk_real_size=disk_car->disk_size;
 #endif
+#ifndef __FRAMAC__
     log_info("New geometry\n%s sector_size=%u\n", disk_car->description(disk_car), disk_car->sector_size);
+#endif
     autoset_unit(disk_car);
     if(geo_modified==2)
     {
+      /*@ assert valid_read_string(*current_cmd); */
       return 1;
     }
   }
+  /*@ assert valid_read_string(*current_cmd); */
   return 0;
 }

src/geometry.h

@@ -27,6 +27,7 @@ extern "C" {
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires 0 < disk->geom.sectors_per_head;
   @ requires 0 < disk->geom.heads_per_cylinder;
   @ assigns disk->geom.cylinders;
@@ -35,19 +36,20 @@ void set_cylinders_from_size_up(disk_t *disk);
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ assigns disk->sector_size, disk->geom.cylinders;
   @*/
 int change_sector_size(disk_t *disk, const int cyl_modified, const unsigned int sector_size);
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid_function(disk->description);
   @ requires \valid(current_cmd);
   @ requires valid_read_string(*current_cmd);
-  @ requires separation: \separated(disk, current_cmd);
+  @ requires separation: \separated(disk, current_cmd, *current_cmd);
-  @ requires \valid_function(disk->description);
-  @ ensures  valid_read_string(*current_cmd);
   @*/
+// ensures  valid_read_string(*current_cmd);
 int change_geometry_cli(disk_t *disk, char **current_cmd);
 
 #ifdef __cplusplus

src/gfs2.h

@@ -79,8 +79,21 @@ struct gfs2_sb {
 	uint8_t sb_uuid[16]; /* The UUID, maybe 0 for backwards compat */
 };
 
-//
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 int check_gfs2(disk_t *disk_car, partition_t *partition);
+
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(sb);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, sb, partition);
+  @*/
 int recover_gfs2(const disk_t *disk_car, const struct gfs2_sb *sb, partition_t *partition, const int dump_ind);
 
 #ifdef __cplusplus

src/godmode.h

@@ -26,7 +26,19 @@ extern "C" {
 #endif
 
 typedef enum part_offset part_offset_t;
-int interface_recovery(disk_t *disk_car, const list_part_t * list_part_org, const int verbose, const int dump_ind, const int align, const int ask_part_order, const unsigned int expert, char **current_cmd);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires valid_list_part(list_part_org);
+  @ requires \separated(disk_car, list_part_org);
+  @*/
+int interface_recovery(disk_t *disk_car, const list_part_t *list_part_org, const int verbose, const int dump_ind, const int align, const int ask_part_order, const unsigned int expert, char **current_cmd);
+
+/*@
+  @ requires valid_list_part(list_part);
+  @ requires valid_list_part(part_boot);
+  @*/
 void only_one_bootable( list_part_t *list_part, const list_part_t *part_boot);
 
 #ifdef __cplusplus

src/hdaccess.h

@@ -26,9 +26,11 @@ extern "C" {
 #endif
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires disk_car->sector_size > 0;
   @ requires disk_car->geom.heads_per_cylinder > 0;
   @ requires \valid_function(disk_car->pread);
+  @ ensures  valid_disk(disk_car);
   @*/
 void hd_update_geometry(disk_t *disk_car, const int verbose);
 
@@ -38,35 +40,30 @@ void hd_update_geometry(disk_t *disk_car, const int verbose);
 void hd_update_all_geometry(const list_disk_t * list_disk, const int verbose);
 
 /*@
-  @ requires list_disk==\null || \valid_read(list_disk);
+  @ requires valid_list_disk(list_disk);
-  @ ensures \result==\null || \valid_read(\result);
+  @ ensures  valid_list_disk(\result);
   @*/
 list_disk_t *hd_parse(list_disk_t *list_disk, const int verbose, const int testdisk_mode);
 
 /*@
   @ requires valid_read_string(device);
-  @ ensures \result==\null || \valid(\result);
+  @ ensures  valid_disk(\result);
-  @ ensures \result!=\null ==> (0 < \result->geom.cylinders < 0x2000000000000);
+  @ ensures  \result!=\null ==> (0 < \result->geom.cylinders < 0x2000000000000);
-  @ ensures \result!=\null ==> (0 < \result->geom.heads_per_cylinder <= 255);
+  @ ensures  \result!=\null ==> (0 < \result->geom.heads_per_cylinder <= 255);
-  @ ensures \result!=\null ==> (0 < \result->geom.sectors_per_head <= 63);
+  @ ensures  \result!=\null ==> (0 < \result->geom.sectors_per_head <= 63);
-  @ ensures \result!=\null ==> valid_read_string(\result->device);
+  @ ensures  valid_disk(\result);
-  @ ensures \result!=\null ==> \freeable(\result);
-  @ ensures \result!=\null ==> (\result->device == \null || \freeable(\result->device));
-  @ ensures \result!=\null ==> (\result->model == \null || \freeable(\result->model));
-  @ ensures \result!=\null ==> (\result->serial_no == \null || \freeable(\result->serial_no));
-  @ ensures \result!=\null ==> (\result->fw_rev == \null || \freeable(\result->fw_rev));
-  @ ensures \result!=\null ==> (\result->data == \null || \freeable(\result->data));
-  @ ensures \result!=\null ==> (\result->rbuffer == \null || \freeable(\result->rbuffer));
-  @ ensures \result!=\null ==> (\result->wbuffer == \null || \freeable(\result->wbuffer));
   @*/
 disk_t *file_test_availability(const char *device, const int verbose, const int testdisk_mode);
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires 0 < disk_car->geom.heads_per_cylinder;
   @ requires 0 < disk_car->geom.sectors_per_head;
   @ requires 0 < disk_car->sector_size;
   @ ensures 0 < disk_car->geom.cylinders < 0x2000000000000;
+  @ ensures  valid_disk(disk_car);
+  @ assigns disk_car->disk_real_size, disk_car->geom.cylinders, disk_car->disk_size;
   @*/
 void update_disk_car_fields(disk_t *disk_car);
 
@@ -97,14 +94,9 @@ void init_disk(disk_t *disk);
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \freeable(disk);
-  @ requires disk->device == \null || \freeable(disk->device);
+  @ requires valid_disk(disk);
-  @ requires disk->model == \null || \freeable(disk->model);
-  @ requires disk->serial_no == \null || \freeable(disk->serial_no);
-  @ requires disk->fw_rev == \null || \freeable(disk->fw_rev);
-  @ requires disk->data == \null || \freeable(disk->data);
-  @ requires disk->rbuffer == \null || \freeable(disk->rbuffer);
-  @ requires disk->wbuffer == \null || \freeable(disk->wbuffer);
   @*/
 void generic_clean(disk_t *disk);
 

src/hdcache.c

@@ -62,13 +62,9 @@ struct cache_struct
   unsigned int  last_io_error_nbr;
 };
 
-static int cache_pread(disk_t *disk_car, void *buffer, const unsigned int count, const uint64_t offset);
-static int cache_pwrite(disk_t *disk_car, const void *buffer, const unsigned int count, const uint64_t offset);
-static int cache_sync(disk_t *disk);
-static void cache_clean(disk_t *disk);
-
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid((char *)buffer + (0 .. count-1));
   @ requires separation: \separated(disk_car, (char *)buffer + (0 .. count-1));
   @*/
@@ -182,6 +178,7 @@ static int cache_pread_aux(disk_t *disk_car, void *buffer, const unsigned int co
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid((char *)buffer + (0 .. count-1));
   @ requires separation: \separated(disk_car, (char *)buffer + (0 .. count-1));
   @*/
@@ -193,6 +190,7 @@ static int cache_pread(disk_t *disk_car, void *buffer, const unsigned int count,
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read((char *)buffer + (0 .. count-1));
   @ requires separation: \separated(disk_car, (const char *)buffer + (0 .. count-1));
   @*/
@@ -215,6 +213,7 @@ static int cache_pwrite(disk_t *disk_car, const void *buffer, const unsigned int
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @*/
 static void cache_clean(disk_t *disk_car)
 {
@@ -267,6 +266,7 @@ static void dup_geometry(CHSgeometry_t * CHS_dst, const CHSgeometry_t * CHS_sour
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ ensures valid_read_string(\result);
   @*/
 static const char *cache_description(disk_t *disk_car)
@@ -282,6 +282,7 @@ static const char *cache_description(disk_t *disk_car)
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ ensures valid_read_string(\result);
   @*/
 static const char *cache_description_short(disk_t *disk_car)

src/hdcache.h

@@ -27,6 +27,7 @@ extern "C" {
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ ensures \valid(\result);
   @*/
 disk_t *new_diskcache(disk_t *disk_car, const unsigned int cache_size_min);

src/hdwin32.h

@@ -26,6 +26,10 @@ extern "C" {
 #endif
 
 #if defined(__CYGWIN__) || defined(__MINGW32__)
+/*@
+  @ requires \valid(dev);
+  @ requires valid_disk(dev);
+  @*/
 void file_win32_disk_get_model(HANDLE handle, disk_t *dev, const int verbose);
 #endif
 

src/hfs.h

@@ -78,6 +78,7 @@ struct hfs_mdb {
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
   @*/
@@ -85,6 +86,7 @@ int check_HFS(disk_t *disk_car, partition_t *partition, const int verbose);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(hfs_mdb);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, hfs_mdb, partition);
@@ -93,6 +95,7 @@ int test_HFS(const disk_t *disk_car, const hfs_mdb_t *hfs_mdb, const partition_t
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(hfs_mdb);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, hfs_mdb, partition);

src/hidden.c

@@ -40,11 +40,14 @@ int is_hpa_or_dco(const disk_t *disk)
   }
   else if(disk->dco > 0 && disk->user_max < disk->dco+1)
   {
+#ifndef __FRAMAC__
     log_info("user_max=%llu dco=%llu\n",
 	(long long unsigned) disk->user_max,
 	(long long unsigned) disk->dco);
+#endif
     res|=2;
   }
+#ifndef __FRAMAC__
   if(res>0)
   {
     if(res&1)
@@ -53,5 +56,6 @@ int is_hpa_or_dco(const disk_t *disk)
       log_warning("%s: Device Configuration Overlay (DCO) present.\n", disk->device);
     log_flush();
   }
+#endif
   return res;
 }

src/hidden.h

@@ -25,6 +25,11 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid_read(disk);
+  @ requires valid_disk(disk);
+  @ assigns  \nothing;
+  @*/
 int is_hpa_or_dco(const disk_t *disk);
 
 #ifdef __cplusplus

src/hpa_dco.h

@@ -25,6 +25,10 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 void disk_get_hpa_dco(const int hd_h, disk_t *disk_car);
 
 #ifdef __cplusplus

src/hpfs.h

@@ -26,7 +26,21 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(hpfs_header);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, hpfs_header, partition);
+  @*/
 int recover_HPFS(const disk_t *disk_car, const struct fat_boot_sector *hpfs_header, partition_t *partition, const int verbose);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 int check_HPFS(disk_t *disk_car,partition_t *partition, const int verbose);
 
 #ifdef __cplusplus

src/intrf.h

@@ -58,8 +58,28 @@ struct MenuItem
 /* '\014' == ^L */
 #define key_REDRAWKEY 		'\014'
 
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 void log_CHS_from_LBA(const disk_t *disk_car, const unsigned long int pos_LBA);
+
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 const char *aff_part_aux(const unsigned int newline, const disk_t *disk_car, const partition_t *partition);
+
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 void aff_part_buffer(const unsigned int newline, const disk_t *disk_car, const partition_t *partition);
 
 /*@
@@ -77,6 +97,12 @@ uint64_t ask_number_cli(char **current_cmd, const uint64_t val_cur, const uint64
 void screen_buffer_reset(void);
 int screen_buffer_add(const char *_format, ...)  __attribute__ ((format (printf, 1, 2)));
 void screen_buffer_to_log(void);
+
+/*@
+  @ requires \valid_read(partition);
+  @ requires valid_partition(partition);
+  @ assigns \nothing;
+  @*/
 int get_partition_status(const partition_t *partition);
 
 #ifdef __cplusplus

src/intrface.c

@@ -60,7 +60,7 @@ void interface_list(disk_t *disk, const int verbose, const int saveheader, const
   printf("%s\n", disk->description(disk));
   printf(msg_PART_HEADER_LONG);
   list_part=disk->arch->read_part(disk,verbose,saveheader);
-
+  /*@ assert valid_list_part(list_part); */
   for(parts=list_part; parts!=NULL; parts=parts->next)
   {
     const char *msg;

src/intrface.h

@@ -25,7 +25,19 @@
 extern "C" {
 #endif
 
-list_part_t *ask_structure(disk_t *disk_car,list_part_t *list_part, const int verbose, char **current_cmd);
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_list_part(list_part);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(current_cmd);
+  @ requires \separated(disk_car, list_part, current_cmd);
+  @*/
+list_part_t *ask_structure(disk_t *disk_car, list_part_t *list_part, const int verbose, char **current_cmd);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 void interface_list(disk_t *disk_car, const int verbose, const int saveheader, const int backup);
 
 #ifdef __cplusplus

src/intrfn.h

@@ -43,8 +43,20 @@ extern "C" {
 
 void aff_copy(WINDOW *window);
 void aff_copy_short(WINDOW *window);
+
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 void aff_LBA2CHS(const disk_t *disk_car, const unsigned long int pos_LBA);
+
+/*@
+  @ requires \valid(window);
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 void aff_part(WINDOW *window, const unsigned int newline, const disk_t *disk_car, const partition_t *partition);
+
 uint64_t ask_number(const uint64_t val_cur, const uint64_t val_min, const uint64_t val_max, const char * _format, ...) __attribute__ ((format (printf, 4, 5)));
 int ask_YN(WINDOW *window);
 int ask_confirmation(const char*_format, ...) __attribute__ ((format (printf, 1, 2)));
@@ -69,7 +81,10 @@ uint64_t ask_int_ncurses(const char *string);
 const char *ask_string_ncurses(const char *string);
 #endif
 
+/*@ assigns \nothing; */
 const char *td_curses_version(void);
+
+/*@ requires valid_read_string(msg); */
 void display_message(const char*msg);
 
 #ifdef __cplusplus

src/io_redir.c

@@ -55,8 +55,19 @@ struct info_io_redir
   list_redir_t *list_redir;
 };
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid((char *)buffer + (0 .. count-1));
+  @ requires separation: \separated(disk_car, (char *)buffer + (0 .. count-1));
+  @*/
 static int io_redir_pread(disk_t *disk_car, void *buffer, const unsigned int count, const uint64_t offset);
-static void io_redir_clean(disk_t *clean);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
+static void io_redir_clean(disk_t *disk_car);
 
 int io_redir_add_redir(disk_t *disk_car, const uint64_t org_offset, const unsigned int size, const uint64_t new_offset, const void *mem)
 {

src/io_redir.h

@@ -25,7 +25,16 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 int io_redir_add_redir(disk_t *disk_car, const uint64_t org_offset, const unsigned int size, const uint64_t new_offset, const void *mem);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 int io_redir_del_redir(disk_t *disk_car, uint64_t org_offset);
 #ifdef __cplusplus
 } /* closing brace for extern "C" */

src/iso.c

@@ -37,8 +37,18 @@
 #include "log.h"
 #include "guid_cpy.h"
 
+/*@
+  @ requires \valid_read(iso);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(iso, partition);
+  @*/
 static void set_ISO_info(const struct iso_primary_descriptor *iso, partition_t *partition);
 
+/*@
+  @ requires \valid_read(iso);
+  @ assigns  \nothing;
+  @*/
 static int test_ISO(const struct iso_primary_descriptor *iso)
 {
   static const unsigned char iso_header[6]= { 0x01, 'C', 'D', '0', '0', '1'};

src/iso.h

@@ -27,7 +27,9 @@ extern "C" {
 #endif
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(disk_car, partition);
   @*/
 int check_ISO(disk_t *disk_car, partition_t *partition);
@@ -35,6 +37,7 @@ int check_ISO(disk_t *disk_car, partition_t *partition);
 /*@
   @ requires \valid_read(iso);
   @ requires \valid(partition);
+  @ requires valid_partition(partition);
   @ requires separation: \separated(iso, partition);
   @*/
 int recover_ISO(const struct iso_primary_descriptor *iso, partition_t *partition);

src/jfs.h

@@ -30,6 +30,7 @@ extern "C" {
 #define L2BPERDMAP 13      /* l2 num of blks per dmap */
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
   @*/
@@ -37,6 +38,7 @@ int check_JFS(disk_t *disk_car, partition_t *partition);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(sb);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, sb, partition);

src/list_sort.h

@@ -23,6 +23,9 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(head);
+  @*/
 void td_list_sort(struct td_list_head *head,
     int (*cmp)(const struct td_list_head *a, const struct td_list_head *b));
 

src/log.c

@@ -54,14 +54,10 @@
 static FILE *log_handle=NULL;
 static int f_status=0;
 
-/*@
-  @ requires valid_read_string(_format);
-  @*/
-static int log_handler(const char *_format, va_list ap) __attribute__((format(printf, 1, 0)));
-
 /* static unsigned int log_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; */
 static unsigned int log_levels=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;
 
+/*@ assigns log_levels; */
 unsigned int log_set_levels(const unsigned int levels)
 {
   const unsigned int old_levels=log_levels;
@@ -69,6 +65,11 @@ unsigned int log_set_levels(const unsigned int levels)
   return old_levels;
 }
 
+/*@
+  @ requires separation: \separated(default_filename, errsv, log_handle, &errno);
+  @ assigns log_handle;
+  @ assigns \result,errno,*errsv;
+  @*/
 int log_open(const char*default_filename, const int mode, int *errsv)
 {
   log_handle=fopen(default_filename,(mode==TD_LOG_CREATE?"w":"a"));
@@ -93,6 +94,11 @@ int log_open(const char*default_filename, const int mode, int *errsv)
   return 1;
 }
 
+/*@
+  @ requires separation: \separated(default_filename, errsv, log_handle, &errno);
+  @ assigns log_handle;
+  @ assigns \result,errno,*errsv;
+  @*/
 #if defined(__CYGWIN__) || defined(__MINGW32__)
 int log_open_default(const char*default_filename, const int mode, int *errsv)
 {
@@ -124,6 +130,9 @@ int log_open_default(const char*default_filename, const int mode, int *errsv)
 #else
 int log_open_default(const char*default_filename, const int mode, int *errsv)
 {
+#ifdef __FRAMAC__
+  return log_open(default_filename, mode, errsv);
+#else
   char*filename;
   char *path;
   int result;
@@ -137,14 +146,26 @@ int log_open_default(const char*default_filename, const int mode, int *errsv)
   result=log_open(filename, mode, errsv);
   free(filename);
   return result;
+#endif
 }
 #endif
 
+/*@
+  @ requires log_handle==\null || \valid(log_handle);
+  @*/
 int log_flush(void)
 {
   return fflush(log_handle);
 }
 
+/*@
+  @ requires \valid(log_handle);
+  @ requires valid_read_string(_format);
+  @ assigns f_status, *log_handle;
+  @*/
+// assigns *log_handle \from _format[..], ap;
+static int log_handler(const char *_format, va_list ap) __attribute__((format(printf, 1, 0)));
+
 static int log_handler(const char *_format, va_list ap)
 {
   int res;
@@ -164,6 +185,11 @@ static int log_handler(const char *_format, va_list ap)
   return res;
 }
 
+/*@
+  @ requires log_handle == \null || \valid(log_handle);
+  @ assigns \result,errno,log_handle;
+  @ assigns f_status;
+  @*/
 int log_close(void)
 {
   if(log_handle!=NULL)
@@ -175,6 +201,11 @@ int log_close(void)
   return f_status;
 }
 
+/*@
+  @ requires log_handle == \null || \valid(log_handle);
+  @ assigns *log_handle;
+  @ assigns f_status;
+  @*/
 int log_redirect(const unsigned int level, const char *format, ...)
 {
   if((log_levels & level)==0)
@@ -191,7 +222,7 @@ int log_redirect(const unsigned int level, const char *format, ...)
   }
 }
 
-void dump_log(const void *nom_dump,unsigned int lng)
+void dump_log(const void *nom_dump, const unsigned int lng)
 {
   unsigned int i,j;
   unsigned int nbr_line;

src/log.h

@@ -30,14 +30,14 @@ unsigned int log_set_levels(const unsigned int levels);
 /*@
   @ requires valid_read_string(default_filename);
   @ requires \valid(errsv);
-  @ requires separation: \separated(default_filename, errsv);
+  @ requires separation: \separated(default_filename, errsv, &errno);
   @*/
 int log_open(const char*default_filename, const int mode, int *errsv);
 
 /*@
   @ requires \valid_read(default_filename);
   @ requires \valid(errsv);
-  @ requires separation: \separated(default_filename, errsv);
+  @ requires separation: \separated(default_filename, errsv, &errno);
   @*/
 int log_open_default(const char*default_filename, const int mode, int *errsv);
 
@@ -48,7 +48,16 @@ int log_close(void);
   @ requires valid_read_string(format);
   @*/
 int log_redirect(const unsigned int level, const char *format, ...) __attribute__((format(printf, 2, 3)));
-void dump_log(const void *nom_dump,unsigned int lng);
+
+/*@
+  @ requires \valid((char *)nom_dump + (0 .. lng-1));
+  @*/
+void dump_log(const void *nom_dump, const unsigned int lng);
+
+/*@
+  @ requires \valid((char *)dump_1 + (0 .. lng-1));
+  @ requires \valid((char *)dump_2 + (0 .. lng-1));
+  @*/
 void dump2_log(const void *dump_1, const void *dump_2,const unsigned int lng);
 
 #define TD_LOG_NONE	0

src/log_part.h

@@ -25,7 +25,18 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid_read(disk);
+  @ requires valid_disk(disk);
+  @ requires \valid_read(partition);
+  @*/
 void log_partition(const disk_t *disk, const partition_t *partition);
+
+/*@
+  @ requires \valid_read(disk);
+  @ requires valid_disk(disk);
+  @ requires valid_list_part(list_part);
+  @*/
 void log_all_partitions(const disk_t *disk, const list_part_t *list_part);
 
 #ifdef __cplusplus

src/lvm.h

@@ -92,14 +92,18 @@ typedef struct {
 #define pv_disk_t pv_disk_v2_t
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
   @*/
 int check_LVM(disk_t *disk_car, partition_t *partition, const int verbose);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(pv);
   @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
   @*/
 int recover_LVM(const disk_t *disk_car, const pv_disk_t *pv, partition_t *partition, const int verbose, const int dump_ind);
 
@@ -130,6 +134,7 @@ struct lvm2_pv_header {
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
   @*/
@@ -137,6 +142,7 @@ int check_LVM2(disk_t *disk_car, partition_t *partition, const int verbose);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(buf);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, buf, partition);

src/md.h

@@ -255,6 +255,7 @@ static inline uint64_t md_event(mdp_super_t *sb) {
 /* TestDisk */
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
   @*/
@@ -262,6 +263,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(sb);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, sb, partition);
@@ -270,6 +272,7 @@ int recover_MD(const disk_t *disk_car, const struct mdp_superblock_s *sb, partit
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
   @*/

src/memmem.h

@@ -40,6 +40,7 @@ static inline const void *td_memmem(const void *haystack, const unsigned int hay
   if (needle_len == 0)
     /* The first occurrence of the empty string is deemed to occur at
        the beginning of the string.  */
+    /*@ assert (\subset((char *)haystack, (char *)haystack+(0..haystack_len-needle_len)) && \valid_read((char *)haystack)); */
     return (const void *) haystack;
 
   /* Sanity check, otherwise the loop might search through the whole
@@ -48,9 +49,12 @@ static inline const void *td_memmem(const void *haystack, const unsigned int hay
     return NULL;
 
   /*@
+    @ loop invariant \valid_read(begin);
+    @ loop invariant \subset(begin, (char *)haystack+(0..haystack_len-needle_len+1));
     @ loop assigns begin;
     @*/
   for (begin = (const char *) haystack; begin <= last_possible; ++begin)
+  {
     if (begin[0] == ((const char *) needle)[0] &&
         !memcmp ((const void *) &begin[1],
                  (const void *) ((const char *) needle + 1),
@@ -59,6 +63,7 @@ static inline const void *td_memmem(const void *haystack, const unsigned int hay
       /*@ assert (\subset(begin, (char *)haystack+(0..haystack_len-needle_len)) && \valid_read(begin)); */
       return (const void *) begin;
     }
+  }
   return NULL;
 }
 #endif

src/msdos.h

@@ -34,6 +34,11 @@ struct info_disk_struct
 };
 
 disk_t *hd_identify(const int verbose, const unsigned int disk, const int testdisk_mode);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 const char *disk_description(disk_t *disk_car);
 
 #ifdef __cplusplus

src/netware.h

@@ -36,6 +36,7 @@ struct disk_netware
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
   @*/
@@ -43,6 +44,7 @@ int check_netware(disk_t *disk_car, partition_t *partition);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(netware_block);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, netware_block, partition);

src/next.h

@@ -25,6 +25,10 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @*/
 void search_location_init(const disk_t *disk_car, const unsigned int location_boundary, const int fast_mode);
 uint64_t search_location_update(const uint64_t location);
 

src/ntfs.c

@@ -184,6 +184,10 @@ int test_NTFS(const disk_t *disk_car, const struct ntfs_boot_sector*ntfs_header,
   return 0;
 }
 
+/*@
+  @ requires \valid_read(record);
+  @ assigns  \nothing;
+  @*/
 static const ntfs_attribheader *ntfs_getattributeheaders(const ntfs_recordheader* record)
 {
   const char* location = (const char*)record;
@@ -195,11 +199,16 @@ static const ntfs_attribheader *ntfs_getattributeheaders(const ntfs_recordheader
   return (const ntfs_attribheader *)location;
 }
 
+/*@
+  @ requires \valid_read(attrib);
+  @ assigns  \nothing;
+  @*/
 static const ntfs_attribheader* ntfs_searchattribute(const ntfs_attribheader* attrib, uint32_t attrType, const char* end, int skip)
 {
   if(attrib==NULL)
     return NULL;
   /* Now we should be at attributes */
+  /*@ loop assigns attrib; */
   while((const char *)attrib + sizeof(ntfs_attribheader) < end &&
       le32(attrib->type)!= 0xffffffff)
   {

src/ntfs_adv.h

@@ -1,6 +1,6 @@
 /*
 
-    File: ntfs.h
+    File: ntfs_adv.h
 
     Copyright (C) 1998-2006,2008 Christophe GRENIER <grenier@cgsecurity.org>
 

src/ntfs_dir.h

@@ -25,7 +25,17 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 dir_partition_t dir_partition_ntfs_init(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const int verbose, const int expert);
+
+/*@
+  @ assigns \nothing;
+  @*/
 const char*td_ntfs_version(void);
 
 #ifdef __cplusplus

src/ntfs_fix.h

@@ -25,6 +25,12 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 int repair_MFT(disk_t *disk_car, partition_t *partition, const int verbose, const unsigned int expert, char **current_cmd);
 
 #ifdef __cplusplus

src/ntfs_udl.h

@@ -25,6 +25,12 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(partition);
+  @ requires \separated(disk_car, partition);
+  @*/
 int ntfs_undelete_part(disk_t *disk_car, const partition_t *partition, const int verbose, char **current_cmd);
 
 #ifdef __cplusplus

src/ntfsp.h

@@ -25,7 +25,16 @@
 extern "C" {
 #endif
 
-unsigned int ntfs_remove_used_space(disk_t *disk_car,const partition_t *partition, alloc_data_t *list_search_space);
+#if defined(HAVE_LIBNTFS) || defined(HAVE_LIBNTFS3G)
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires valid_list_search_space(list_search_space);
+  @ requires \separated(disk_car, partition, list_search_space);
+  @ ensures  valid_list_search_space(list_search_space);
+  @*/
+unsigned int ntfs_remove_used_space(disk_t *disk_car, const partition_t *partition, alloc_data_t *list_search_space);
+#endif
 
 #ifdef __cplusplus
 } /* closing brace for extern "C" */

src/ole.h

@@ -1,6 +1,6 @@
 /*
 
-    File: common.c
+    File: ole.h
 
     Copyright (C) 2006 Christophe GRENIER <grenier@cgsecurity.org>
   

src/partauto.h

@@ -27,8 +27,11 @@ extern "C" {
 
 /*@
   @ requires \valid(disk);
+  @ requires valid_disk(disk);
   @ requires \valid_read(arch);
+  @ requires valid_disk(disk);
   @ requires separation: \separated(disk, arch);
+  @ ensures  valid_disk(disk);
   @*/
 void autodetect_arch(disk_t *disk, const arch_fnct_t *arch);
 

src/partgptn.h

@@ -25,6 +25,12 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires valid_list_part(list_part);
+  @ ensures  valid_list_part(list_part);
+  @*/
 list_part_t *add_partition_gpt_ncurses(disk_t *disk, list_part_t *list_part);
 
 #ifdef __cplusplus

src/parthumax.c

@@ -45,11 +45,14 @@
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @*/
+// ensures  valid_list_part(\result);
 static list_part_t *read_part_humax(disk_t *disk_car, const int verbose, const int saveheader);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(list_part);
   @ requires separation: \separated(disk_car, list_part);
   @*/
@@ -72,7 +75,6 @@ static void set_next_status_humax(const disk_t *disk_car, partition_t *partition
 
 /*@
   @ requires list_part == \null || \valid_read(list_part);
-  @ assigns \nothing;
   @*/
 static int test_structure_humax(const list_part_t *list_part);
 
@@ -160,6 +162,7 @@ static list_part_t *read_part_humax(disk_t *disk_car, const int verbose, const i
   list_part_t *new_list_part=NULL;
   uint32_t *p32;
   unsigned char *buffer;
+  /*@ assert valid_list_part(new_list_part); */
   if(disk_car->sector_size < DEFAULT_SECTOR_SIZE)
     return NULL;
   buffer=(unsigned char *)MALLOC(disk_car->sector_size);
@@ -181,6 +184,9 @@ static list_part_t *read_part_humax(disk_t *disk_car, const int verbose, const i
     free(buffer);
     return NULL;
   }
+  /*@
+    @ loop invariant valid_list_part(new_list_part);
+    @*/
   for(i=0;i<4;i++)
   {
      if (humaxlabel->partitions[i].num_sectors > 0)
@@ -241,10 +247,14 @@ list_part_t *add_partition_humax_cli(const disk_t *disk_car,list_part_t *list_pa
   end.cylinder=disk_car->geom.cylinders-1;
   end.head=disk_car->geom.heads_per_cylinder-1;
   end.sector=disk_car->geom.sectors_per_head;
-  /*@ loop invariant valid_read_string(*current_cmd); */
+  /*@
+    @ loop invariant valid_list_part(list_part);
+    @ loop invariant valid_read_string(*current_cmd);
+    @ */
   while(1)
   {
     skip_comma_in_command(current_cmd);
+    /*@ assert valid_read_string(*current_cmd); */
     if(check_command(current_cmd,"c,",2)==0)
     {
       start.cylinder=ask_number_cli(current_cmd, start.cylinder,0,disk_car->geom.cylinders-1,"Enter the starting cylinder ");
@@ -262,19 +272,25 @@ list_part_t *add_partition_humax_cli(const disk_t *disk_car,list_part_t *list_pa
     {
       int insert_error=0;
       list_part_t *new_list_part=insert_new_partition(list_part, new_partition, 0, &insert_error);
+      /*@ assert valid_list_part(new_list_part); */
       if(insert_error>0)
       {
 	free(new_partition);
+	/*@ assert valid_list_part(new_list_part); */
 	return new_list_part;
       }
       new_partition->status=STATUS_PRIM;
       if(test_structure_humax(list_part)!=0)
 	new_partition->status=STATUS_DELETED;
+      /*@ assert valid_read_string(*current_cmd); */
+      /*@ assert valid_list_part(new_list_part); */
       return new_list_part;
     }
     else
     {
       free(new_partition);
+      /*@ assert valid_read_string(*current_cmd); */
+      /*@ assert valid_list_part(list_part); */
       return list_part;
     }
   }

src/parti386.c

@@ -144,6 +144,8 @@ static int diff(const unsigned char buffer[DEFAULT_SECTOR_SIZE], const unsigned
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ ensures  valid_list_part(\result);
   @*/
 static list_part_t *read_part_i386(disk_t *disk_car, const int verbose, const int saveheader);
 
@@ -528,6 +530,7 @@ static list_part_t *read_part_i386(disk_t *disk_car, const int verbose, const in
   CHSgeometry_t geometry;
   list_part_t *new_list_part=NULL;
   unsigned char *buffer=(unsigned char *)MALLOC(disk_car->sector_size);
+  /*@ assert valid_list_part(new_list_part); */
   screen_buffer_reset();
   if((unsigned)disk_car->pread(disk_car, buffer, disk_car->sector_size, (uint64_t)0) != disk_car->sector_size)
   {
@@ -544,6 +547,9 @@ static list_part_t *read_part_i386(disk_t *disk_car, const int verbose, const in
     free(buffer);
     return NULL;
   }
+  /*@
+    @ loop invariant valid_list_part(new_list_part);
+    @*/
   for(i=0;i<4;i++)
   {
     const struct partition_dos *p=pt_offset(buffer,i);
@@ -1183,27 +1189,27 @@ static void partition2_i386_entry(const disk_t *disk_car, const uint64_t pos, co
   if(start.cylinder>1023)
   { /* Partition Magic 5 uses CHS=(1023,0,1) if extended or last logical *
      * Linux fdisk and TestDisk use CHS=(1023,lastH,lastS)               */
-    p->head=(unsigned char)disk_car->geom.heads_per_cylinder-1;
+    p->head=(disk_car->geom.heads_per_cylinder-1)&0xff;
-    p->sector=(unsigned char)(disk_car->geom.sectors_per_head | ((1023>>8)<<6));
+    p->sector=(disk_car->geom.sectors_per_head | ((1023>>8)<<6))&0xff;
-    p->cyl=(unsigned char)1023;
+    p->cyl=1023&0xff;
   }
   else
   {
-    p->head=(unsigned char)start.head;
+    p->head=start.head&0xff;
-    p->sector=(unsigned char)(start.sector|((start.cylinder>>8)<<6));
+    p->sector=(start.sector|((start.cylinder>>8)<<6))&0xff;
-    p->cyl=(unsigned char)(start.cylinder);
+    p->cyl=start.cylinder&0xff;
   }
   if(end.cylinder>1023)
   {
-    p->end_head=(unsigned char)disk_car->geom.heads_per_cylinder-1;
+    p->end_head=(disk_car->geom.heads_per_cylinder-1)&0xff;
-    p->end_sector=(unsigned char)(disk_car->geom.sectors_per_head | ((1023>>8)<<6));
+    p->end_sector=(disk_car->geom.sectors_per_head | ((1023>>8)<<6))&0xff;
-    p->end_cyl=(unsigned char)1023;
+    p->end_cyl=1023&0xff;
   }
   else
   {
-    p->end_head=(unsigned char)end.head;
+    p->end_head=end.head&0xff;
-    p->end_sector=(unsigned char)(end.sector|((end.cylinder>>8)<<6));
+    p->end_sector=(end.sector|((end.cylinder>>8)<<6))&0xff;
-    p->end_cyl=(unsigned char)end.cylinder;
+    p->end_cyl=end.cylinder&0xff;
   }
   if((partition->part_size/disk_car->sector_size)<=0xFFFFFFFF)
     set_nr_sects(p,partition->part_size/disk_car->sector_size);
@@ -1405,7 +1411,10 @@ list_part_t *add_partition_i386_cli(disk_t *disk_car, list_part_t *list_part, ch
   end.cylinder=disk_car->geom.cylinders-1;
   end.head=disk_car->geom.heads_per_cylinder-1;
   end.sector=disk_car->geom.sectors_per_head;
-  /*@ loop invariant valid_read_string(*current_cmd); */
+  /*@
+    @ loop invariant valid_list_part(list_part);
+    @ loop invariant valid_read_string(*current_cmd);
+    @ */
   while(1)
   {
     skip_comma_in_command(current_cmd);
@@ -1449,9 +1458,12 @@ list_part_t *add_partition_i386_cli(disk_t *disk_car, list_part_t *list_part, ch
     {
       int insert_error=0;
       list_part_t *new_list_part=insert_new_partition(list_part, new_partition, 0, &insert_error);
+      /*@ assert valid_list_part(new_list_part); */
       if(insert_error>0)
       {
 	free(new_partition);
+	/*@ assert valid_read_string(*current_cmd); */
+	/*@ assert valid_list_part(new_list_part); */
 	return new_list_part;
       }
       if(test_structure_i386(list_part)==0)
@@ -1460,21 +1472,37 @@ list_part_t *add_partition_i386_cli(disk_t *disk_car, list_part_t *list_part, ch
 	{
 	  new_partition->status=STATUS_LOG;
 	  if(test_structure_i386(new_list_part)==0)
+	  {
+	    /*@ assert valid_read_string(*current_cmd); */
+	    /*@ assert valid_list_part(new_list_part); */
 	    return new_list_part;
+	  }
 	}
 	new_partition->status=STATUS_PRIM_BOOT;
 	if(test_structure_i386(new_list_part)==0)
+	{
+	  /*@ assert valid_read_string(*current_cmd); */
+	  /*@ assert valid_list_part(new_list_part); */
 	  return new_list_part;
+	}
 	new_partition->status=STATUS_PRIM;
 	if(test_structure_i386(new_list_part)==0)
+	{
+	  /*@ assert valid_read_string(*current_cmd); */
+	  /*@ assert valid_list_part(new_list_part); */
 	  return new_list_part;
+	}
       }
       new_partition->status=STATUS_DELETED;
+      /*@ assert valid_read_string(*current_cmd); */
+      /*@ assert valid_list_part(new_list_part); */
       return new_list_part;
     }
     else
     {
       free(new_partition);
+      /*@ assert valid_read_string(*current_cmd); */
+      /*@ assert valid_list_part(list_part); */
       return list_part;
     }
   }

src/parti386.h

@@ -33,13 +33,15 @@ extern "C" {
 int parti386_can_be_ext(const disk_t *disk_car, const partition_t *partition);
 
 /*@
-  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
-  @ requires list_part == \null || \valid_read(list_part);
+  @ requires \valid_read(disk_car);
+  @ requires valid_list_part(list_part);
   @ requires \valid(current_cmd);
+  @ requires separation: \separated(disk_car, list_part, current_cmd, *current_cmd);
   @ requires valid_read_string(*current_cmd);
-  @ requires separation: \separated(disk_car, list_part, current_cmd);
-  @ ensures  valid_read_string(*current_cmd);
   @*/
+// ensures  valid_list_part(\result);
+// ensures  valid_read_string(*current_cmd);
 list_part_t *add_partition_i386_cli(disk_t *disk_car, list_part_t *list_part, char **current_cmd);
 
 /*@

src/parti386n.h

@@ -25,6 +25,11 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires valid_disk(disk);
+  @ requires valid_list_part(list_part);
+  @ ensures  valid_list_part(\result);
+  @*/
 list_part_t *add_partition_i386_ncurses(disk_t *disk, list_part_t *list_part);
 
 #ifdef __cplusplus

src/partmac.c

@@ -56,6 +56,8 @@ static int check_part_mac(disk_t *disk_car, const int verbose,partition_t *parti
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ ensures  valid_list_part(\result);
   @*/
 static list_part_t *read_part_mac(disk_t *disk_car, const int verbose, const int saveheader);
 
@@ -275,6 +277,10 @@ list_part_t *add_partition_mac_cli(disk_t *disk_car,list_part_t *list_part, char
   assert(current_cmd!=NULL);
   new_partition->part_offset=disk_car->sector_size;
   new_partition->part_size=disk_car->disk_size-disk_car->sector_size;
+  /*@
+    @ loop invariant valid_list_part(list_part);
+    @ loop invariant valid_read_string(*current_cmd);
+    @ */
   while(1)
   {
     skip_comma_in_command(current_cmd);
@@ -310,19 +316,23 @@ list_part_t *add_partition_mac_cli(disk_t *disk_car,list_part_t *list_part, char
     {
       int insert_error=0;
       list_part_t *new_list_part=insert_new_partition(list_part, new_partition, 0, &insert_error);
+      /*@ assert valid_list_part(new_list_part); */
       if(insert_error>0)
       {
 	free(new_partition);
+	/*@ assert valid_list_part(new_list_part); */
 	return new_list_part;
       }
       new_partition->status=STATUS_PRIM;
       if(test_structure_mac(list_part)!=0)
 	new_partition->status=STATUS_DELETED;
+      /*@ assert valid_list_part(new_list_part); */
       return new_list_part;
     }
     else
     {
       free(new_partition);
+      /*@ assert valid_list_part(list_part); */
       return list_part;
     }
   }

src/partmacn.h

@@ -27,6 +27,11 @@ extern "C" {
 #endif
 
 void write_part_mac_warning_ncurses(void);
+/*@
+  @ requires valid_disk(disk);
+  @ requires valid_list_part(list_part);
+  @ ensures  valid_list_part(list_part);
+  @*/
 list_part_t *add_partition_mac_ncurses(disk_t *disk, list_part_t *list_part);
 
 #ifdef __cplusplus

src/partsun.c

@@ -62,7 +62,9 @@ static int get_geometry_from_sunmbr(const unsigned char *buffer, const int verbo
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @*/
+// ensures  valid_list_part(\result);
 static list_part_t *read_part_sun(disk_t *disk_car, const int verbose, const int saveheader);
 
 /*@
@@ -87,7 +89,6 @@ static void set_next_status_sun(const disk_t *disk_car, partition_t *partition);
 
 /*@
   @ requires list_part == \null || \valid_read(list_part);
-  @ assigns \nothing;
   @*/
 static int test_structure_sun(const list_part_t *list_part);
 
@@ -200,6 +201,7 @@ static list_part_t *read_part_sun(disk_t *disk_car, const int verbose, const int
   sun_disklabel *sunlabel;
   list_part_t *new_list_part=NULL;
   unsigned char *buffer;
+  /*@ assert valid_list_part(new_list_part); */
   if(disk_car->sector_size < DEFAULT_SECTOR_SIZE)
     return NULL;
   buffer=(unsigned char *)MALLOC(disk_car->sector_size);
@@ -217,6 +219,9 @@ static list_part_t *read_part_sun(disk_t *disk_car, const int verbose, const int
     free(buffer);
     return NULL;
   }
+  /*@
+    @ loop invariant valid_list_part(new_list_part);
+    @*/
   for(i=0;i<8;i++)
   {
      if (sunlabel->partitions[i].num_sectors > 0
@@ -238,6 +243,7 @@ static list_part_t *read_part_sun(disk_t *disk_car, const int verbose, const int
      }
   }
   free(buffer);
+  /*@ assert valid_list_part(new_list_part); */
   return new_list_part;
 }
 
@@ -294,7 +300,10 @@ list_part_t *add_partition_sun_cli(const disk_t *disk_car,list_part_t *list_part
   end.cylinder=disk_car->geom.cylinders-1;
   end.head=disk_car->geom.heads_per_cylinder-1;
   end.sector=disk_car->geom.sectors_per_head;
-  /*@ loop invariant valid_read_string(*current_cmd); */
+  /*@
+    @ loop invariant valid_list_part(list_part);
+    @ loop invariant valid_read_string(*current_cmd);
+    @ */
   while(1)
   {
     skip_comma_in_command(current_cmd);
@@ -315,19 +324,23 @@ list_part_t *add_partition_sun_cli(const disk_t *disk_car,list_part_t *list_part
     {
       int insert_error=0;
       list_part_t *new_list_part=insert_new_partition(list_part, new_partition, 0, &insert_error);
+      /*@ assert valid_list_part(new_list_part); */
       if(insert_error>0)
       {
 	free(new_partition);
+	/*@ assert valid_list_part(new_list_part); */
 	return new_list_part;
       }
       new_partition->status=STATUS_PRIM;
       if(test_structure_sun(list_part)!=0)
 	new_partition->status=STATUS_DELETED;
+      /*@ assert valid_list_part(new_list_part); */
       return new_list_part;
     }
     else
     {
       free(new_partition);
+      /*@ assert valid_list_part(list_part); */
       return list_part;
     }
   }

src/partsunn.h

@@ -25,6 +25,11 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires valid_disk(disk);
+  @ requires valid_list_part(list_part);
+  @ ensures  valid_list_part(list_part);
+  @*/
 list_part_t *add_partition_sun_ncurses(disk_t *disk, list_part_t *list_part);
 
 #ifdef __cplusplus

src/partxbox.c

@@ -53,7 +53,9 @@ static int check_part_xbox(disk_t *disk_car, const int verbose,partition_t *part
 
 /*@
   @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
   @*/
+// ensures  valid_list_part(\result);
 static list_part_t *read_part_xbox(disk_t *disk_car, const int verbose, const int saveheader);
 
 /*@
@@ -80,7 +82,6 @@ static void set_next_status_xbox(const disk_t *disk_car, partition_t *partition)
 
 /*@
   @ requires list_part == \null || \valid_read(list_part);
-  @ assigns \nothing;
   @*/
 static int test_structure_xbox(const list_part_t *list_part);
 
@@ -156,6 +157,7 @@ static list_part_t *read_part_xbox(disk_t *disk_car, const int verbose, const in
 {
   unsigned char buffer[0x800];
   list_part_t *new_list_part=NULL;
+  /*@ assert valid_list_part(new_list_part); */
   screen_buffer_reset();
   if(disk_car->pread(disk_car, &buffer, sizeof(buffer), 0) != sizeof(buffer))
     return new_list_part;
@@ -168,6 +170,9 @@ static list_part_t *read_part_xbox(disk_t *disk_car, const int verbose, const in
       screen_buffer_add("\nBad XBOX partition, invalid signature\n");
       return NULL;
     }
+    /*@
+      @ loop invariant valid_list_part(new_list_part);
+      @*/
     for(i=0;i<sizeof(offsets)/sizeof(uint64_t);i++)
     {
       if(offsets[i]<disk_car->disk_size)
@@ -190,6 +195,7 @@ static list_part_t *read_part_xbox(disk_t *disk_car, const int verbose, const in
       }
     }
   }
+  /*@ assert valid_list_part(new_list_part); */
   return new_list_part;
 }
 
@@ -212,7 +218,10 @@ list_part_t *add_partition_xbox_cli(const disk_t *disk_car,list_part_t *list_par
   assert(current_cmd!=NULL);
   new_partition->part_offset=disk_car->sector_size;
   new_partition->part_size=disk_car->disk_size-disk_car->sector_size;
-  /*@ loop invariant valid_read_string(*current_cmd); */
+  /*@
+    @ loop invariant valid_list_part(list_part);
+    @ loop invariant valid_read_string(*current_cmd);
+    @ */
   while(1)
   {
     skip_comma_in_command(current_cmd);
@@ -248,19 +257,23 @@ list_part_t *add_partition_xbox_cli(const disk_t *disk_car,list_part_t *list_par
     {
       int insert_error=0;
       list_part_t *new_list_part=insert_new_partition(list_part, new_partition, 0, &insert_error);
+      /*@ assert valid_list_part(new_list_part); */
       if(insert_error>0)
       {
 	free(new_partition);
+	/*@ assert valid_list_part(new_list_part); */
 	return new_list_part;
       }
       new_partition->status=STATUS_PRIM;
       if(test_structure_xbox(list_part)!=0)
 	new_partition->status=STATUS_DELETED;
+      /*@ assert valid_list_part(new_list_part); */
       return new_list_part;
     }
     else
     {
       free(new_partition);
+      /*@ assert valid_list_part(list_part); */
       return list_part;
     }
   }

src/partxboxn.h

@@ -25,6 +25,11 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires valid_disk(disk_car);
+  @ requires valid_list_part(list_part);
+  @ ensures  valid_list_part(list_part);
+  @*/
 list_part_t *add_partition_xbox_ncurses(disk_t *disk, list_part_t *list_part);
 
 #ifdef __cplusplus

src/pdisksel.c

@@ -40,6 +40,10 @@ disk_t *photorec_disk_selection_cli(const char *cmd_device, const list_disk_t *l
 {
   const list_disk_t *element_disk;
   disk_t *disk=NULL;
+  /*@
+    @ loop invariant valid_disk(disk);
+    @ loop assigns element_disk, disk;
+    @*/
   for(element_disk=list_disk;element_disk!=NULL;element_disk=element_disk->next)
   {
     if(strcmp(element_disk->disk->device, cmd_device)==0)

src/pdisksel.h

@@ -25,6 +25,14 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires valid_read_string(cmd_device);
+  @ requires \valid_read(list_disk);
+  @ requires valid_disk(list_disk->disk);
+  @ requires \valid(list_search_space);
+  @ requires \separated(cmd_device, list_disk, list_search_space);
+  @ ensures  valid_disk(\result);
+  @*/
 disk_t *photorec_disk_selection_cli(const char *cmd_device, const list_disk_t *list_disk, alloc_data_t *list_search_space);
 
 #ifdef __cplusplus

src/pdiskseln.c

@@ -337,7 +337,7 @@ int do_curses_photorec(struct ph_param *params, struct ph_options *options, cons
       return 0;
     }
     change_arch_type_cli(params->disk, options->verbose, &params->cmd_run);
-    autoset_unit(disk);
+    autoset_unit(params->disk);
     menu_photorec(params, options, &list_search_space);
     /*@ assert params->cmd_run == \null || valid_read_string(params->cmd_run); */
     return 0;

src/pdiskseln.h

@@ -27,12 +27,16 @@ extern "C" {
 
 /*@
   @ requires \valid(params);
+  @ requires valid_ph_param(params);
   @ requires \valid(options);
-  @ requires list_disk == \null || \valid_read(list_disk);
+  @ requires list_disk == \null || (\valid_read(list_disk) && valid_disk(list_disk->disk));
   @ requires params->cmd_device==\null || valid_read_string(params->cmd_device);
   @ requires params->cmd_run==\null || valid_read_string(params->cmd_run);
+  @ requires params->disk==\null;
+  @ requires \separated(params, options, list_disk);
   @ ensures  params->cmd_run==\null || valid_read_string(params->cmd_run);
   @*/
+// ensures  params->disk==\null || valid_disk(params->disk);
 int do_curses_photorec(struct ph_param *params, struct ph_options *options, const list_disk_t *list_disk);
 
 #ifdef __cplusplus

src/phbs.c

@@ -58,6 +58,11 @@ extern const file_hint_t file_hint_tar;
 extern file_check_list_t file_check_list;
 extern int need_to_stop;
 
+/*@
+  @ requires \valid(dst);
+  @ requires \valid_read(src);
+  @ requires \separated(src, dst);
+  @*/
 static inline void file_recovery_cpy(file_recovery_t *dst, const file_recovery_t *src)
 {
   memcpy(dst, src, sizeof(*dst));

src/phbs.h

@@ -25,6 +25,12 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(params);
+  @ requires \valid_read(options);
+  @ requires valid_list_search_space(list_search_space);
+  @ requires \separated(params, options, list_search_space);
+  @*/
 pstatus_t photorec_find_blocksize(struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space);
 
 #ifdef __cplusplus

src/phcfg.h

@@ -25,8 +25,19 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(files_enable);
+  @*/
 void reset_array_file_enable(file_enable_t *files_enable);
+
+/*@
+  @ requires \valid_read(files_enable);
+  @*/
 int file_options_save(const file_enable_t *files_enable);
+
+/*@
+  @ requires \valid(files_enable);
+  @*/
 int file_options_load(file_enable_t *files_enable);
 
 #ifdef __cplusplus

src/phcli.h

@@ -27,10 +27,19 @@ extern "C" {
 
 /*@
   @ requires \valid(list_part);
+  @ requires valid_list_part(list_part);
   @ requires \valid(params);
+  @ requires valid_ph_param(params);
+  @ requires valid_disk(params->disk);
+  @ requires \valid_function(params->disk->description);
   @ requires \valid(options);
   @ requires \valid(list_search_space);
+  @ requires valid_read_string(params->cmd_run);
+  @ requires \valid_function(params->disk->description);
+  @ requires valid_list_search_space(list_search_space);
+  @ requires \separated(&need_to_stop, list_part, params, options, list_search_space);
   @*/
+// ensures  valid_list_search_space(list_search_space);
 int menu_photorec_cli(list_part_t *list_part, struct ph_param *params, struct ph_options *options, alloc_data_t*list_search_space);
 
 #ifdef __cplusplus