From b2a0d41da609e62865beec1ed6faddd12bb5bdb8 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sat, 20 Nov 2021 11:26:50 +0100 Subject: [PATCH] Numerous frama-c annotations --- src/alignio.h | 18 +++- src/analyse.h | 103 +++++++++++++++++++++ src/autoset.h | 1 + src/bfs.h | 2 + src/bsd.h | 2 + src/btrfs.h | 15 ++- src/chgarch.h | 4 + src/chgtype.h | 8 ++ src/chgtypen.h | 6 ++ src/cramfs.h | 14 +++ src/dimage.h | 7 ++ src/dir.c | 49 +++++++++- src/dir.h | 65 ++++++++++++- src/dirn.h | 6 ++ src/dirpart.h | 6 ++ src/diskacc.h | 5 + src/diskcapa.h | 4 + src/edit.h | 4 + src/ewf.h | 5 + src/exfat.c | 5 + src/exfat.h | 32 +++++++ src/exfat_dir.h | 6 ++ src/exfatp.c | 5 + src/exfatp.h | 9 ++ src/ext2_common.h | 1 + src/f2fs.h | 18 ++++ src/fat.c | 95 +++++++++++++++---- src/fat.h | 21 +++++ src/fat1x.h | 6 ++ src/fat32.h | 6 ++ src/fat_adv.h | 22 ++++- src/fat_cluster.h | 22 ++++- src/fat_dir.c | 58 +++++++++++- src/fat_dir.h | 15 +++ src/fatp.c | 24 +++++ src/fatp.h | 9 ++ src/fatx.h | 12 +++ src/fidentify.c | 1 + src/file_txt.c | 1 + src/filegen.c | 17 +++- src/filegen.h | 17 +++- src/geometry.c | 24 ++++- src/geometry.h | 8 +- src/gfs2.h | 15 ++- src/godmode.h | 14 ++- src/hdaccess.h | 36 +++----- src/hdcache.c | 11 ++- src/hdcache.h | 1 + src/hdwin32.h | 4 + src/hfs.h | 3 + src/hidden.c | 4 + src/hidden.h | 5 + src/hpa_dco.h | 4 + src/hpfs.h | 14 +++ src/intrf.h | 26 ++++++ src/intrface.c | 2 +- src/intrface.h | 14 ++- src/intrfn.h | 15 +++ src/io_redir.c | 13 ++- src/io_redir.h | 9 ++ src/iso.c | 10 ++ src/iso.h | 3 + src/jfs.h | 2 + src/list_sort.h | 3 + src/log.c | 43 +++++++-- src/log.h | 15 ++- src/log_part.h | 11 +++ src/lvm.h | 6 ++ src/md.h | 3 + src/memmem.h | 5 + src/msdos.h | 5 + src/netware.h | 2 + src/next.h | 4 + src/ntfs.c | 9 ++ src/ntfs_adv.h | 2 +- src/ntfs_dir.h | 10 ++ src/ntfs_fix.h | 6 ++ src/ntfs_udl.h | 6 ++ src/ntfsp.h | 11 ++- src/ole.h | 2 +- src/partauto.h | 3 + src/partgptn.h | 6 ++ src/parthumax.c | 20 +++- src/parti386.c | 54 ++++++++--- src/parti386.h | 10 +- src/parti386n.h | 5 + src/partmac.c | 10 ++ src/partmacn.h | 5 + src/partsun.c | 17 +++- src/partsunn.h | 5 + src/partxbox.c | 17 +++- src/partxboxn.h | 5 + src/pdisksel.c | 4 + src/pdisksel.h | 8 ++ src/pdiskseln.c | 2 +- src/pdiskseln.h | 6 +- src/phbs.c | 5 + src/phbs.h | 6 ++ src/phcfg.h | 11 +++ src/phcli.h | 9 ++ src/phmain.c | 1 + src/photorec.c | 117 ++++++++++++++++++++++-- src/photorec.h | 176 +++++++++++++++++++++++++++++++++++- src/photorec_check_header.h | 45 +++++++-- src/phrecn.h | 9 ++ src/pnext.h | 28 ++++++ src/ppartseln.h | 10 ++ src/psearch.h | 20 ++++ src/psearchn.h | 7 ++ src/savehdr.h | 13 +++ src/sessionp.c | 9 +- src/sessionp.h | 23 ++++- src/setdate.h | 5 + src/tanalyse.c | 1 + src/tanalyse.h | 4 + src/tload.h | 4 + src/tpartwr.h | 4 + src/unicode.h | 11 +++ 118 files changed, 1664 insertions(+), 137 deletions(-) diff --git a/src/alignio.h b/src/alignio.h index 72996b29..be949e26 100644 --- a/src/alignio.h +++ b/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); - @ ensures disk_car->rbuffer == \null || (\freeable(disk_car->rbuffer) && disk_car->rbuffer_size > 0); + @ requires \separated(disk_car, (char *)buf); + @ 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); - @ ensures disk_car->wbuffer == \null || \freeable(disk_car->wbuffer); + @ requires \separated(disk_car, (char *)buf); + @ 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 diff --git a/src/analyse.h b/src/analyse.h index 782076b9..6b3f3836 100644 --- a/src/analyse.h +++ b/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 diff --git a/src/autoset.h b/src/autoset.h index 9dccbeb2..a7f512bf 100644 --- a/src/autoset.h +++ b/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); diff --git a/src/bfs.h b/src/bfs.h index f631fcc4..fb3dd7d0 100644 --- a/src/bfs.h +++ b/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); diff --git a/src/bsd.h b/src/bsd.h index 4554864a..52c9f02c 100644 --- a/src/bsd.h +++ b/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); diff --git a/src/btrfs.h b/src/btrfs.h index dad5511f..022c6962 100644 --- a/src/btrfs.h +++ b/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 diff --git a/src/chgarch.h b/src/chgarch.h index a6892db1..505763a4 100644 --- a/src/chgarch.h +++ b/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); diff --git a/src/chgtype.h b/src/chgtype.h index 668cf7fb..3365eb51 100644 --- a/src/chgtype.h +++ b/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 diff --git a/src/chgtypen.h b/src/chgtypen.h index ef9f4180..1afe8f06 100644 --- a/src/chgtypen.h +++ b/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 diff --git a/src/cramfs.h b/src/cramfs.h index dc126957..eef22aae 100644 --- a/src/cramfs.h +++ b/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 diff --git a/src/dimage.h b/src/dimage.h index ac304d24..1b588b2f 100644 --- a/src/dimage.h +++ b/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 diff --git a/src/dir.c b/src/dir.c index 7501627d..2a2e3090 100644 --- a/src/dir.c +++ b/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; ipart_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; diff --git a/src/exfat.h b/src/exfat.h index fb39e9e0..29e0eee1 100644 --- a/src/exfat.h +++ b/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 diff --git a/src/exfat_dir.h b/src/exfat_dir.h index 9ea2b137..ee3e0810 100644 --- a/src/exfat_dir.h +++ b/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 diff --git a/src/exfatp.c b/src/exfatp.c index 06c24ec2..edcb36a2 100644 --- a/src/exfatp.c +++ b/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; ifsname[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 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; diff --git a/src/fat_dir.h b/src/fat_dir.h index af2ac030..9e1d34a5 100644 --- a/src/fat_dir.h +++ b/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 diff --git a/src/fatp.c b/src/fatp.c index 179bedeb..a227082e 100644 --- a/src/fatp.c +++ b/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; diff --git a/src/fatp.h b/src/fatp.h index 2b62af0e..699a25e3 100644 --- a/src/fatp.h +++ b/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 diff --git a/src/fatx.h b/src/fatx.h index 1fb3d72c..a6c46ac9 100644 --- a/src/fatx.h +++ b/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 diff --git a/src/fidentify.c b/src/fidentify.c index 50036c87..1b3d4dfb 100644 --- a/src/fidentify.c +++ b/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; diff --git a/src/file_txt.c b/src/file_txt.c index 005b4d62..8c3984ea 100644 --- a/src/file_txt.c +++ b/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; diff --git a/src/filegen.c b/src/filegen.c index aacac1c0..fbd51c74 100644 --- a/src/filegen.c +++ b/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_function(file_check_new->header_check); + @ requires valid_file_check_node(file_check_new); @*/ 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(¤t_check->offset) && \initialized(¤t_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); diff --git a/src/filegen.h b/src/filegen.h index 6fe571aa..4fbbcf5f 100644 --- a/src/filegen.h +++ b/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 */ - /* side effect for data_check_flv */ + /* data_check modifies file_recovery->calculated_file_size, it can also update data_check, file_check, offset_error, offset_ok, time, data_check_tmp */ 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, diff --git a/src/geometry.c b/src/geometry.c index 98f4d752..8759feb7 100644 --- a/src/geometry.c +++ b/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)) - log_error("Illegal sector size\n"); - else + if(change_sector_size(disk_car, cyl_modified, tmp_val)==0) 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; } diff --git a/src/geometry.h b/src/geometry.h index 1cf32e7b..c196e447 100644 --- a/src/geometry.h +++ b/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 \valid_function(disk->description); - @ ensures valid_read_string(*current_cmd); + @ requires separation: \separated(disk, current_cmd, *current_cmd); @*/ +// ensures valid_read_string(*current_cmd); int change_geometry_cli(disk_t *disk, char **current_cmd); #ifdef __cplusplus diff --git a/src/gfs2.h b/src/gfs2.h index 7e439bfd..b3a7af05 100644 --- a/src/gfs2.h +++ b/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 diff --git a/src/godmode.h b/src/godmode.h index 0527b150..bf95ba46 100644 --- a/src/godmode.h +++ b/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 diff --git a/src/hdaccess.h b/src/hdaccess.h index f1431b03..81d1c011 100644 --- a/src/hdaccess.h +++ b/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); - @ ensures \result==\null || \valid_read(\result); + @ requires valid_list_disk(list_disk); + @ 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 \result!=\null ==> (0 < \result->geom.cylinders < 0x2000000000000); - @ ensures \result!=\null ==> (0 < \result->geom.heads_per_cylinder <= 255); - @ ensures \result!=\null ==> (0 < \result->geom.sectors_per_head <= 63); - @ ensures \result!=\null ==> valid_read_string(\result->device); - @ 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)); + @ ensures valid_disk(\result); + @ ensures \result!=\null ==> (0 < \result->geom.cylinders < 0x2000000000000); + @ ensures \result!=\null ==> (0 < \result->geom.heads_per_cylinder <= 255); + @ ensures \result!=\null ==> (0 < \result->geom.sectors_per_head <= 63); + @ ensures valid_disk(\result); @*/ 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 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); + @ requires valid_disk(disk); @*/ void generic_clean(disk_t *disk); diff --git a/src/hdcache.c b/src/hdcache.c index e2bc8621..af66339d 100644 --- a/src/hdcache.c +++ b/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) diff --git a/src/hdcache.h b/src/hdcache.h index c2d9b238..d263f4bc 100644 --- a/src/hdcache.h +++ b/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); diff --git a/src/hdwin32.h b/src/hdwin32.h index f78d55de..1057f68d 100644 --- a/src/hdwin32.h +++ b/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 diff --git a/src/hfs.h b/src/hfs.h index 3020f97d..cc500d2f 100644 --- a/src/hfs.h +++ b/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); diff --git a/src/hidden.c b/src/hidden.c index 919ec1fa..de2940fd 100644 --- a/src/hidden.c +++ b/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; } diff --git a/src/hidden.h b/src/hidden.h index 4d302bdc..f5bda2e0 100644 --- a/src/hidden.h +++ b/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 diff --git a/src/hpa_dco.h b/src/hpa_dco.h index 783e46e6..944670e3 100644 --- a/src/hpa_dco.h +++ b/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 diff --git a/src/hpfs.h b/src/hpfs.h index faee3aec..0e950801 100644 --- a/src/hpfs.h +++ b/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 diff --git a/src/intrf.h b/src/intrf.h index 2bc4f9e6..dd9cfe30 100644 --- a/src/intrf.h +++ b/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 diff --git a/src/intrface.c b/src/intrface.c index 4375d0cf..b5c7203f 100644 --- a/src/intrface.c +++ b/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; diff --git a/src/intrface.h b/src/intrface.h index cc860075..96e3208a 100644 --- a/src/intrface.h +++ b/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 diff --git a/src/intrfn.h b/src/intrfn.h index 064fadef..9d928b9b 100644 --- a/src/intrfn.h +++ b/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 diff --git a/src/io_redir.c b/src/io_redir.c index 2e34562a..5fa867a9 100644 --- a/src/io_redir.c +++ b/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) { diff --git a/src/io_redir.h b/src/io_redir.h index 7c83d237..1130fbcb 100644 --- a/src/io_redir.h +++ b/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" */ diff --git a/src/iso.c b/src/iso.c index 05b636c4..d7809048 100644 --- a/src/iso.c +++ b/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'}; diff --git a/src/iso.h b/src/iso.h index 38d96847..bd3e94ff 100644 --- a/src/iso.h +++ b/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); diff --git a/src/jfs.h b/src/jfs.h index 16244bf5..55967025 100644 --- a/src/jfs.h +++ b/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); diff --git a/src/list_sort.h b/src/list_sort.h index 495a2761..b5a97b89 100644 --- a/src/list_sort.h +++ b/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)); diff --git a/src/log.c b/src/log.c index 25cb32f1..4c4b758e 100644 --- a/src/log.c +++ 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; diff --git a/src/log.h b/src/log.h index 638a304d..087742dd 100644 --- a/src/log.h +++ b/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 diff --git a/src/log_part.h b/src/log_part.h index 0ceadfd1..d233acfa 100644 --- a/src/log_part.h +++ b/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 diff --git a/src/lvm.h b/src/lvm.h index 404925a5..f2bebbf2 100644 --- a/src/lvm.h +++ b/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); diff --git a/src/md.h b/src/md.h index e810fb02..eb579f48 100644 --- a/src/md.h +++ b/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); @*/ diff --git a/src/memmem.h b/src/memmem.h index 3ce9787d..d139d851 100644 --- a/src/memmem.h +++ b/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 diff --git a/src/msdos.h b/src/msdos.h index 83196d6b..78724274 100644 --- a/src/msdos.h +++ b/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 diff --git a/src/netware.h b/src/netware.h index 939a8d32..67b2c4d4 100644 --- a/src/netware.h +++ b/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); diff --git a/src/next.h b/src/next.h index 81dc3440..2dd03993 100644 --- a/src/next.h +++ b/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); diff --git a/src/ntfs.c b/src/ntfs.c index afc4c352..ec2c8f64 100644 --- a/src/ntfs.c +++ b/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) { diff --git a/src/ntfs_adv.h b/src/ntfs_adv.h index 2f1bffe0..b5691a72 100644 --- a/src/ntfs_adv.h +++ b/src/ntfs_adv.h @@ -1,6 +1,6 @@ /* - File: ntfs.h + File: ntfs_adv.h Copyright (C) 1998-2006,2008 Christophe GRENIER diff --git a/src/ntfs_dir.h b/src/ntfs_dir.h index a4a4757c..8f7b534e 100644 --- a/src/ntfs_dir.h +++ b/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 diff --git a/src/ntfs_fix.h b/src/ntfs_fix.h index cb69c15b..8bf18cff 100644 --- a/src/ntfs_fix.h +++ b/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 diff --git a/src/ntfs_udl.h b/src/ntfs_udl.h index 5dc9afa7..7435055b 100644 --- a/src/ntfs_udl.h +++ b/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 diff --git a/src/ntfsp.h b/src/ntfsp.h index c63698f0..fde1e1fb 100644 --- a/src/ntfsp.h +++ b/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" */ diff --git a/src/ole.h b/src/ole.h index 9fb56ca9..6b432636 100644 --- a/src/ole.h +++ b/src/ole.h @@ -1,6 +1,6 @@ /* - File: common.c + File: ole.h Copyright (C) 2006 Christophe GRENIER diff --git a/src/partauto.h b/src/partauto.h index ee2a7eeb..dbd7d7bc 100644 --- a/src/partauto.h +++ b/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); diff --git a/src/partgptn.h b/src/partgptn.h index c63e658c..88af8cb5 100644 --- a/src/partgptn.h +++ b/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 diff --git a/src/parthumax.c b/src/parthumax.c index 4858e6d3..1088a826 100644 --- a/src/parthumax.c +++ b/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; } } diff --git a/src/parti386.c b/src/parti386.c index f7737b83..1ddb5de7 100644 --- a/src/parti386.c +++ b/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->sector=(unsigned char)(disk_car->geom.sectors_per_head | ((1023>>8)<<6)); - p->cyl=(unsigned char)1023; + p->head=(disk_car->geom.heads_per_cylinder-1)&0xff; + p->sector=(disk_car->geom.sectors_per_head | ((1023>>8)<<6))&0xff; + p->cyl=1023&0xff; } else { - p->head=(unsigned char)start.head; - p->sector=(unsigned char)(start.sector|((start.cylinder>>8)<<6)); - p->cyl=(unsigned char)(start.cylinder); + p->head=start.head&0xff; + p->sector=(start.sector|((start.cylinder>>8)<<6))&0xff; + p->cyl=start.cylinder&0xff; } if(end.cylinder>1023) { - p->end_head=(unsigned char)disk_car->geom.heads_per_cylinder-1; - p->end_sector=(unsigned char)(disk_car->geom.sectors_per_head | ((1023>>8)<<6)); - p->end_cyl=(unsigned char)1023; + p->end_head=(disk_car->geom.heads_per_cylinder-1)&0xff; + p->end_sector=(disk_car->geom.sectors_per_head | ((1023>>8)<<6))&0xff; + p->end_cyl=1023&0xff; } else { - p->end_head=(unsigned char)end.head; - p->end_sector=(unsigned char)(end.sector|((end.cylinder>>8)<<6)); - p->end_cyl=(unsigned char)end.cylinder; + p->end_head=end.head&0xff; + p->end_sector=(end.sector|((end.cylinder>>8)<<6))&0xff; + 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; } } diff --git a/src/parti386.h b/src/parti386.h index 2a52a8ec..f8cb990c 100644 --- a/src/parti386.h +++ b/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 list_part == \null || \valid_read(list_part); + @ requires valid_disk(disk_car); + @ 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); /*@ diff --git a/src/parti386n.h b/src/parti386n.h index 6315aecc..51eddb7d 100644 --- a/src/parti386n.h +++ b/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 diff --git a/src/partmac.c b/src/partmac.c index a9f1cbab..eb1cbf36 100644 --- a/src/partmac.c +++ b/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; } } diff --git a/src/partmacn.h b/src/partmacn.h index 802629cc..39b5fb8c 100644 --- a/src/partmacn.h +++ b/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 diff --git a/src/partsun.c b/src/partsun.c index 93e14002..b8fbb4d3 100644 --- a/src/partsun.c +++ b/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; } } diff --git a/src/partsunn.h b/src/partsunn.h index d161a578..de645bf8 100644 --- a/src/partsunn.h +++ b/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 diff --git a/src/partxbox.c b/src/partxbox.c index a9704b43..a28d391a 100644 --- a/src/partxbox.c +++ b/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;idisk_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; } } diff --git a/src/partxboxn.h b/src/partxboxn.h index 61ec166f..7a1bdfe7 100644 --- a/src/partxboxn.h +++ b/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 diff --git a/src/pdisksel.c b/src/pdisksel.c index 69546944..aa86ab25 100644 --- a/src/pdisksel.c +++ b/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) diff --git a/src/pdisksel.h b/src/pdisksel.h index b62049b9..a03ce556 100644 --- a/src/pdisksel.h +++ b/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 diff --git a/src/pdiskseln.c b/src/pdiskseln.c index 5d70bc1b..38f91af9 100644 --- a/src/pdiskseln.c +++ b/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, ¶ms->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; diff --git a/src/pdiskseln.h b/src/pdiskseln.h index e4cf41af..a961b470 100644 --- a/src/pdiskseln.h +++ b/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 diff --git a/src/phbs.c b/src/phbs.c index ad08d20e..269afed1 100644 --- a/src/phbs.c +++ b/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)); diff --git a/src/phbs.h b/src/phbs.h index 031992f9..ee3406a3 100644 --- a/src/phbs.h +++ b/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 diff --git a/src/phcfg.h b/src/phcfg.h index 66a382d6..619bbdc3 100644 --- a/src/phcfg.h +++ b/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 diff --git a/src/phcli.h b/src/phcli.h index 45dc5b07..43addc6e 100644 --- a/src/phcli.h +++ b/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 diff --git a/src/phmain.c b/src/phmain.c index cdd8d7bf..230db573 100644 --- a/src/phmain.c +++ b/src/phmain.c @@ -34,6 +34,7 @@ #undef HAVE_NCURSES #undef ENABLE_DFXML #undef HAVE_SETLOCALE +#undef HAVE_GETEUID #endif #include diff --git a/src/photorec.c b/src/photorec.c index 8a16f95e..0b7006a5 100644 --- a/src/photorec.c +++ b/src/photorec.c @@ -71,7 +71,19 @@ uint64_t gpfh_nbr=0; static void update_search_space_aux(alloc_data_t *list_search_space, uint64_t start, uint64_t end, alloc_data_t **new_current_search_space, uint64_t *offset); + +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_recovery, list_search_space); + @*/ static void file_block_truncate_zero(const file_recovery_t *file_recovery, alloc_data_t *list_search_space); + +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_recovery, list_search_space); + @*/ static int file_block_truncate(const file_recovery_t *file_recovery, alloc_data_t *list_search_space, const unsigned int blocksize); void file_block_log(const file_recovery_t *file_recovery, const unsigned int sector_size) @@ -79,6 +91,7 @@ void file_block_log(const file_recovery_t *file_recovery, const unsigned int sec struct td_list_head *tmp; if(file_recovery->filename[0]=='\0') return; +#ifndef __FRAMAC__ log_info("%s\t",file_recovery->filename); td_list_for_each(tmp, &file_recovery->location.list) { @@ -89,6 +102,7 @@ void file_block_log(const file_recovery_t *file_recovery, const unsigned int sec log_info(" (%lu-%lu)", (unsigned long)(element->start/sector_size), (unsigned long)(element->end/sector_size)); } log_info("\n"); +#endif } void del_search_space(alloc_data_t *list_search_space, const uint64_t start, const uint64_t end) @@ -253,14 +267,15 @@ void free_list_search_space(alloc_data_t *list_search_space) unsigned int photorec_mkdir(const char *recup_dir, const unsigned int initial_dir_num) { - char working_recup_dir[2048]; int dir_ok=0; int dir_num=initial_dir_num; #ifdef DJGPP int i=0; #endif + /*@ loop invariant valid_read_string(recup_dir); */ do { + char working_recup_dir[2048]; snprintf(working_recup_dir,sizeof(working_recup_dir)-1,"%s.%d",recup_dir,dir_num); #ifdef HAVE_MKDIR #ifdef __MINGW32__ @@ -291,6 +306,10 @@ unsigned int photorec_mkdir(const char *recup_dir, const unsigned int initial_di return dir_num; } +/*@ + @ requires \separated(list_search_space, current_search_space, offset, &gpfh_nbr); + @ assigns gpfh_nbr, *current_search_space, *offset; + @ */ int get_prev_file_header(const alloc_data_t *list_search_space, alloc_data_t **current_search_space, uint64_t *offset) { int nbr; @@ -298,17 +317,22 @@ int get_prev_file_header(const alloc_data_t *list_search_space, alloc_data_t **c uint64_t size=0; gpfh_nbr++; /* Search backward the first fragment of a file not successfully recovered - * Limit the search to 10 fragments or 1GB */ + * Limit the search to 3 fragments or 200MB */ + /*@ + @ loop assigns nbr, file_space, *current_search_space, *offset; + @*/ for(nbr=0; nbr<3 && size < (uint64_t)200*1024*1024; nbr++) { file_space=td_list_prev_entry(file_space, list); if(file_space==list_search_space) return -1; + /*@ assert file_space->end > file_space->start; */ size+=file_space->end - file_space->start + 1; if(file_space->file_stat!=NULL) { *current_search_space=file_space; *offset=file_space->start; + /*@ assert *current_search_space!=list_search_space && *offset == (*current_search_space)->start; */ return 0; } } @@ -363,6 +387,9 @@ void update_stats(file_stat_t *file_stats, alloc_data_t *list_search_space) struct td_list_head *search_walker = NULL; int i; /* Reset */ + /*@ + @ loop assigns i, file_stats[i].not_recovered; + @*/ for(i=0;file_stats[i].file_hint!=NULL;i++) file_stats[i].not_recovered=0; /* Update */ @@ -434,10 +461,11 @@ partition_t *new_whole_disk(const disk_t *disk_car) return fake_partition; } -unsigned int find_blocksize(alloc_data_t *list_search_space, const unsigned int default_blocksize, uint64_t *offset) +unsigned int find_blocksize(const alloc_data_t *list_search_space, const unsigned int default_blocksize, uint64_t *offset) { + /* NTFS cluster size can be 2 MB since Windows 10 Creators edition */ + // FIXME unsigned int blocksize=2*1024*1024; unsigned int blocksize=128*512; - struct td_list_head *search_walker = NULL; int run_again; *offset=0; if(td_list_empty(&list_search_space->list)) @@ -445,6 +473,7 @@ unsigned int find_blocksize(alloc_data_t *list_search_space, const unsigned int *offset=(td_list_first_entry(&list_search_space->list, alloc_data_t, list))->start % blocksize; do { + const struct td_list_head *search_walker = NULL; run_again=0; td_list_for_each(search_walker, &list_search_space->list) { @@ -479,6 +508,7 @@ void update_blocksize(const unsigned int blocksize, alloc_data_t *list_search_sp td_list_for_each_prev_safe(search_walker,search_walker_prev,&list_search_space->list) { alloc_data_t *current_search_space=td_list_entry(search_walker, alloc_data_t, list); + /*@ assert current_search_space->start >= offset; */ const uint64_t aligned_start=(current_search_space->start-offset%blocksize+blocksize-1)/blocksize*blocksize+offset%blocksize; if(current_search_space->start!=aligned_start) { @@ -519,7 +549,10 @@ void update_blocksize(const unsigned int blocksize, alloc_data_t *list_search_sp uint64_t free_list_allocation_end=0; -void file_block_free(alloc_list_t *list_allocation) +/*@ + @ requires \valid(list_allocation); + @*/ +static void file_block_free(alloc_list_t *list_allocation) { struct td_list_head *tmp = NULL; struct td_list_head *tmp_next = NULL; @@ -537,14 +570,20 @@ void file_block_free(alloc_list_t *list_allocation) /*@ @ requires \valid(file_recovery); @ requires \valid(params); + @ requires valid_ph_param(params); @ requires \valid(file_recovery->handle); + @ requires valid_file_recovery(file_recovery); + @ requires \separated(file_recovery, params, file_recovery->handle); @*/ static void file_finish_aux(file_recovery_t *file_recovery, struct ph_param *params, const int paranoid) { + /*@ assert valid_file_recovery(file_recovery); */ if(params->status!=STATUS_EXT2_ON_SAVE_EVERYTHING && params->status!=STATUS_EXT2_OFF_SAVE_EVERYTHING && file_recovery->file_stat!=NULL && file_recovery->file_check!=NULL && paranoid>0) { /* Check if recovered file is valid */ + /*@ assert file_recovery->file_check != \null; */ + /*@ assert \valid_function(file_recovery->file_check); */ file_recovery->file_check(file_recovery); } /* FIXME: need to adapt read_size to volume size to avoid this */ @@ -555,10 +594,12 @@ static void file_finish_aux(file_recovery_t *file_recovery, struct ph_param *par if(file_recovery->file_stat!=NULL && file_recovery->file_size> 0 && file_recovery->file_size < file_recovery->min_filesize) { +#ifndef __FRAMAC__ log_info("%s File too small ( %llu < %llu), reject it\n", file_recovery->filename, (long long unsigned) file_recovery->file_size, (long long unsigned) file_recovery->min_filesize); +#endif file_recovery->file_size=0; } if(file_recovery->file_size==0) @@ -568,6 +609,7 @@ static void file_finish_aux(file_recovery_t *file_recovery, struct ph_param *par fclose(file_recovery->handle); file_recovery->handle=NULL; /* File is zero-length; erase it */ + /*@ assert valid_read_string((const char *)file_recovery->filename); */ unlink(file_recovery->filename); return; } @@ -582,8 +624,13 @@ static void file_finish_aux(file_recovery_t *file_recovery, struct ph_param *par file_recovery->handle=NULL; if(file_recovery->time!=0 && file_recovery->time!=(time_t)-1) set_date(file_recovery->filename, file_recovery->time, file_recovery->time); + /*@ assert valid_file_recovery(file_recovery); */ if(file_recovery->file_rename!=NULL) + { + /*@ assert file_recovery->file_rename != \null; */ + /*@ assert \valid_function(file_recovery->file_rename); */ file_recovery->file_rename(file_recovery); + } if((++params->file_nbr)%MAX_FILES_PER_DIR==0) { params->dir_num=photorec_mkdir(params->recup_dir, params->dir_num+1); @@ -643,6 +690,7 @@ void file_recovery_aborted(file_recovery_t *file_recovery, struct ph_param *para { fclose(file_recovery->handle); file_recovery->handle=NULL; + /*@ assert valid_file_recovery(file_recovery); */ /* File is zero-length; erase it */ unlink(file_recovery->filename); } @@ -675,6 +723,7 @@ pfstatus_t file_finish2(file_recovery_t *file_recovery, struct ph_param *params, void info_list_search_space(const alloc_data_t *list_search_space, const alloc_data_t *current_search_space, const unsigned int sector_size, const int keep_corrupted_file, const int verbose) { +#ifndef __FRAMAC__ struct td_list_head *search_walker = NULL; unsigned long int nbr_headers=0; uint64_t sectors_with_unknown_data=0; @@ -703,6 +752,7 @@ void info_list_search_space(const alloc_data_t *list_search_space, const alloc_d log_info("%llu sectors contain unknown data, %lu invalid files found %s.\n", (long long unsigned)sectors_with_unknown_data, (long unsigned)nbr_headers, (keep_corrupted_file>0?"but saved":"and rejected")); +#endif } void free_search_space(alloc_data_t *list_search_space) @@ -738,9 +788,18 @@ void set_filename(file_recovery_t *file_recovery, struct ph_param *params) } } +/*@ + @ requires \valid(new_current_search_space); + @ requires \valid(list_search_space); + @ requires \separated(new_current_search_space, list_search_space); + @ assigns *new_current_search_space; + @*/ static void set_search_start_aux(alloc_data_t **new_current_search_space, alloc_data_t *list_search_space, const uint64_t offset) { struct td_list_head *search_walker = NULL; + /*@ + @ loop assigns search_walker, *new_current_search_space; + @*/ td_list_for_each(search_walker, &list_search_space->list) { alloc_data_t *current_search_space; @@ -759,7 +818,7 @@ static void set_search_start_aux(alloc_data_t **new_current_search_space, alloc_ uint64_t set_search_start(struct ph_param *params, alloc_data_t **new_current_search_space, alloc_data_t *list_search_space) { uint64_t offset=(*new_current_search_space)->start; - if(params->offset!=-1) + if(params->offset!=PH_INVALID_OFFSET) { offset=params->offset; set_search_start_aux(new_current_search_space, list_search_space, offset); @@ -786,7 +845,7 @@ void params_reset(struct ph_param *params, const struct ph_options *options) params->real_start_time=time(NULL); params->dir_num=1; params->file_stats=init_file_stats(options->list_file_format); - params->offset=-1; + params->offset=PH_INVALID_OFFSET; if(params->blocksize==0) params->blocksize=params->disk->sector_size; } @@ -819,7 +878,7 @@ const char *status_to_name(const photorec_status_t status) void status_inc(struct ph_param *params, const struct ph_options *options) { - params->offset=-1; + params->offset=PH_INVALID_OFFSET; switch(params->status) { case STATUS_UNFORMAT: @@ -869,16 +928,24 @@ list_part_t *init_list_part(disk_t *disk, const struct ph_options *options) list_part_t *list_part; partition_t *partition_wd; list_part=disk->arch->read_part(disk, (options!=NULL?options->verbose:0), 0); + /*@ assert valid_list_part(list_part); */ partition_wd=new_whole_disk(disk); list_part=insert_new_partition(list_part, partition_wd, 0, &insert_error); if(insert_error>0) { free(partition_wd); } + /*@ assert valid_list_part(list_part); */ return list_part; } /* file_block_remove_from_sp: remove block from list_search_space, update offset and new_current_search_space in consequence */ +/*@ + @ requires \valid(tmp); + @ requires \valid(new_current_search_space); + @ requires \valid(offset); + @ requires \separated(tmp, new_current_search_space, offset); + @*/ static inline void file_block_remove_from_sp_aux(alloc_data_t *tmp, alloc_data_t **new_current_search_space, uint64_t *offset, const unsigned int blocksize) { if(tmp->start == *offset) @@ -917,6 +984,12 @@ static inline void file_block_remove_from_sp_aux(alloc_data_t *tmp, alloc_data_t } } +/*@ + @ requires \valid(list_search_space); + @ requires \valid(new_current_search_space); + @ requires \valid(offset); + @ requires \separated(list_search_space, new_current_search_space, offset); + @*/ static inline void file_block_remove_from_sp(alloc_data_t *list_search_space, alloc_data_t **new_current_search_space, uint64_t *offset, const unsigned int blocksize) { struct td_list_head *search_walker = &(*new_current_search_space)->list; @@ -945,6 +1018,11 @@ static inline void file_block_remove_from_sp(alloc_data_t *list_search_space, al exit(1); } +/*@ + @ requires \valid(list); + @ requires \valid(list->list.prev); + @ requires offset + blocksize < 0xffffffffffffffff; + @*/ static inline void file_block_add_to_file(alloc_list_t *list, const uint64_t offset, const uint64_t blocksize, const unsigned int data) { if(!td_list_empty(&list->list)) @@ -971,6 +1049,9 @@ void file_block_append(file_recovery_t *file_recovery, alloc_data_t *list_search file_block_remove_from_sp(list_search_space, new_current_search_space, offset, blocksize); } +/*@ + @ requires \valid(list_search_space); + @*/ static void file_block_truncate_aux(const uint64_t start, const uint64_t end, alloc_data_t *list_search_space) { struct td_list_head *search_walker = NULL; @@ -1017,6 +1098,11 @@ static void file_block_truncate_aux(const uint64_t start, const uint64_t end, al } } +/*@ + @ requires \valid(list_search_space); + @ requires \valid(file_stat); + @ requires \separated(list_search_space, file_stat); + @*/ static void file_block_truncate_zero_aux(const uint64_t start, const uint64_t end, alloc_data_t *list_search_space, file_stat_t *file_stat) { struct td_list_head *search_walker = NULL; @@ -1111,6 +1197,10 @@ static int file_block_truncate(const file_recovery_t *file_recovery, alloc_data_ return file_truncated; } +/*@ + @ requires \valid_read(file_recovery); + @ assigns \nothing; + @*/ static uint64_t file_offset_end(const file_recovery_t *file_recovery) { const struct td_list_head *tmp=file_recovery->location.list.prev; @@ -1118,10 +1208,19 @@ static uint64_t file_offset_end(const file_recovery_t *file_recovery) return element->end; } +/*@ + @ requires \valid_read(file_recovery); + @ requires \valid(list_search_space); + @ requires \valid(new_current_search_space); + @ requires \valid(offset); + @ requires \separated(file_recovery, list_search_space, new_current_search_space, offset); + @ assigns *new_current_search_space, *offset; + @*/ static void file_block_move(const file_recovery_t *file_recovery, alloc_data_t *list_search_space, alloc_data_t **new_current_search_space, uint64_t *offset) { const uint64_t end=file_offset_end(file_recovery); struct td_list_head *tmp; + /*@ loop assigns tmp; */ td_list_for_each(tmp, &list_search_space->list) { alloc_data_t *element=td_list_entry(tmp, alloc_data_t, list); @@ -1156,6 +1255,8 @@ void file_block_truncate_and_move(file_recovery_t *file_recovery, alloc_data_t * if(fread(block_buffer, blocksize, 1, file_recovery->handle) != 1) return ; file_recovery->data_check(buffer, 2*blocksize, file_recovery); + if(file_recovery->data_check==NULL) + return ; memcpy(buffer, block_buffer, blocksize); } } diff --git a/src/photorec.h b/src/photorec.h index 7b3345df..84cbb503 100644 --- a/src/photorec.h +++ b/src/photorec.h @@ -64,61 +64,227 @@ struct ph_param uint64_t offset; }; +/*@ + predicate valid_ph_param(struct ph_param *p) = (\valid_read(p) && + (p->recup_dir == \null || valid_read_string(p->recup_dir)) + ); + @*/ + +#define PH_INVALID_OFFSET 0xffffffffffffffff + +/*@ + @ requires valid_list_search_space(list_search_space); + @ requires \separated(list_search_space, current_search_space, offset); + @ requires current_search_space==\null || (\valid(*current_search_space) && valid_list_search_space(*current_search_space)); + @ ensures \result==0 ==> (*current_search_space!=list_search_space && *offset == (*current_search_space)->start); + @*/ +// ensures current_search_space==\null || (\valid(*current_search_space) && valid_list_search_space(*current_search_space)); int get_prev_file_header(const alloc_data_t *list_search_space, alloc_data_t **current_search_space, uint64_t *offset); + +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_recovery, params, list_search_space); + @*/ int file_finish_bf(file_recovery_t *file_recovery, struct ph_param *params, alloc_data_t *list_search_space); + +/*@ + @ requires \valid(file_recovery); + @ requires valid_file_recovery(file_recovery); + @ requires valid_list_search_space(list_search_space); + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \separated(file_recovery, params, list_search_space, &errno); + @*/ void file_recovery_aborted(file_recovery_t *file_recovery, struct ph_param *params, alloc_data_t *list_search_space); /*@ @ requires \valid(file_recovery); + @ requires valid_file_recovery(file_recovery); @ requires \valid(params); - @ requires \valid(list_search_space); - @ ensures \result == PFSTATUS_BAD || \result == PFSTATUS_OK || \result == PFSTATUS_OK_TRUNCATED; + @ requires valid_ph_param(params); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_recovery, params, list_search_space); + @ ensures \result == PFSTATUS_BAD || \result == PFSTATUS_OK || \result == PFSTATUS_OK_TRUNCATED; @*/ +// ensures valid_file_recovery(file_recovery); pfstatus_t file_finish2(file_recovery_t *file_recovery, struct ph_param *params, const int paranoid, alloc_data_t *list_search_space); +/*@ + @ requires \valid_read(file_stats); + @*/ void write_stats_log(const file_stat_t *file_stats); + +/*@ + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_stats, list_search_space); + @*/ +//ensures valid_list_search_space(list_search_space); void update_stats(file_stat_t *file_stats, alloc_data_t *list_search_space); +/*@ + @ requires \valid_read(disk_car); + @ requires valid_disk(disk_car); + @*/ +// ensures valid_partition(\result); partition_t *new_whole_disk(const disk_t *disk_car); -unsigned int find_blocksize(alloc_data_t *list_file, const unsigned int default_blocksize, uint64_t *offset); + +/*@ + @ requires valid_list_search_space(list_file); + @ requires \valid(offset); + @ requires \separated(list_file, offset); + @ requires default_blocksize > 0; + @*/ +// ensures \result > 0; +unsigned int find_blocksize(const alloc_data_t *list_file, const unsigned int default_blocksize, uint64_t *offset); + +/*@ + @ requires blocksize > 0; + @ requires valid_list_search_space(list_search_space); + @*/ void update_blocksize(const unsigned int blocksize, alloc_data_t *list_search_space, const uint64_t offset); + +/*@ + @ requires valid_list_search_space(list_search_space); + @ requires current_search_space==\null || valid_list_search_space(current_search_space); + @*/ +// ensures current_search_space==\null || valid_list_search_space(current_search_space); void forget(const alloc_data_t *list_search_space, alloc_data_t *current_search_space); /*@ - @ requires \valid(list_search_space); + @ requires valid_list_search_space(list_search_space); @ requires \valid_read(disk_car); + @ requires valid_disk(disk_car); @ requires disk_car->disk_size > 0; @ requires disk_car->disk_real_size > 0; @ requires \valid_read(partition); @ requires separation: \separated(list_search_space, disk_car, partition); @*/ void init_search_space(alloc_data_t *list_search_space, const disk_t *disk_car, const partition_t *partition); + +/*@ + @ 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); + @ ensures valid_disk(disk_car); + @ ensures valid_list_search_space(list_search_space); + @*/ unsigned int remove_used_space(disk_t *disk_car, const partition_t *partition, alloc_data_t *list_search_space); + +/*@ + @ requires valid_list_search_space(list_search_space); + @*/ void free_list_search_space(alloc_data_t *list_search_space); + int sorfile_stat_ts(const void *p1, const void *p2); + +/*@ + @ requires valid_read_string(recup_dir); + @ requires \separated(recup_dir, &errno); + @*/ unsigned int photorec_mkdir(const char *recup_dir, const unsigned int initial_dir_num); + +/*@ + @ requires valid_list_search_space(list_search_space); + @ requires \separated(list_search_space, current_search_space); + @ ensures valid_list_search_space(list_search_space); + @*/ void info_list_search_space(const alloc_data_t *list_search_space, const alloc_data_t *current_search_space, const unsigned int sector_size, const int keep_corrupted_file, const int verbose); + +/*@ + @ requires valid_list_search_space(list_search_space); + @*/ void free_search_space(alloc_data_t *list_search_space); + +/*@ + @ requires \valid(file_recovery); + @ requires valid_file_recovery(file_recovery); + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \separated(file_recovery, params); + @*/ +// ensures valid_file_recovery(file_recovery); void set_filename(file_recovery_t *file_recovery, struct ph_param *params); + +/*@ + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(params, new_current_search_space, list_search_space); + @ requires new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); + @*/ +// ensures new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); +// ensures valid_list_search_space(list_search_space); uint64_t set_search_start(struct ph_param *params, alloc_data_t **new_current_search_space, alloc_data_t *list_search_space); + +/*@ + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \valid_read(options); + @ requires \separated(params, options); + @*/ void params_reset(struct ph_param *params, const struct ph_options *options); + +/*@ + @ assigns \nothing; + @*/ const char *status_to_name(const photorec_status_t status); + +/*@ + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \valid_read(options); + @ requires \separated(params, options); + @ assigns params->offset, params->status, params->file_nbr; + @*/ void status_inc(struct ph_param *params, const struct ph_options *options); /*@ @ requires \valid(disk); + @ requires valid_disk(disk); @ requires \valid_read(&disk->arch); @ requires \valid_function(disk->arch->read_part); @ requires \valid_read(options); + @ requires \separated(disk, options); + @ ensures valid_disk(disk); @*/ +// ensures valid_list_part(\result); list_part_t *init_list_part(disk_t *disk, const struct ph_options *options); + +/*@ + @ requires valid_file_recovery(file_recovery); + @*/ +// ensures valid_file_recovery(file_recovery); void file_block_log(const file_recovery_t *file_recovery, const unsigned int sector_size); -void file_block_free(alloc_list_t *list_allocation); + +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_recovery, list_search_space, new_current_search_space, offset); + @ requires new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); + @*/ +// ensures new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); +// ensures valid_file_recovery(file_recovery); +// ensures valid_list_search_space(list_search_space); void file_block_append(file_recovery_t *file_recovery, alloc_data_t *list_search_space, alloc_data_t **new_current_search_space, uint64_t *offset, const unsigned int blocksize, const unsigned int data); + +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_recovery, list_search_space, new_current_search_space, offset, buffer + (..)); + @ requires new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); + @*/ +// ensures new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); +// ensures valid_file_recovery(file_recovery); +// ensures valid_list_search_space(list_search_space); void file_block_truncate_and_move(file_recovery_t *file_recovery, alloc_data_t *list_search_space, const unsigned int blocksize, alloc_data_t **new_current_search_space, uint64_t *offset, unsigned char *buffer); /*@ @ requires \valid(list_search_space); + @ requires valid_list_search_space(list_search_space); @*/ void del_search_space(alloc_data_t *list_search_space, const uint64_t start, const uint64_t end); diff --git a/src/photorec_check_header.h b/src/photorec_check_header.h index 203641eb..a13ba3ce 100644 --- a/src/photorec_check_header.h +++ b/src/photorec_check_header.h @@ -61,6 +61,9 @@ static FILE *fopen_with_retry(const char *path, const char *mode) } #endif +/*@ + @ requires \valid_read(buffer + (0 .. read_size-1)); + @*/ static void photorec_dir_fat(const unsigned char *buffer, const unsigned int read_size, const unsigned long long sector) { file_info_t dir_list; @@ -68,7 +71,9 @@ static void photorec_dir_fat(const unsigned char *buffer, const unsigned int rea dir_fat_aux(buffer, read_size, 0, &dir_list); if(!td_list_empty(&dir_list.list)) { +#ifndef __FRAMAC__ log_info("Sector %llu\n", sector); +#endif dir_aff_log(NULL, &dir_list); delete_list_file(&dir_list); } @@ -76,20 +81,19 @@ static void photorec_dir_fat(const unsigned char *buffer, const unsigned int rea /*@ @ requires \valid_read(file_recovery_new); + @ requires valid_file_recovery(file_recovery_new); @ requires \valid(file_recovery); - @ requires file_recovery->extension == \null || valid_read_string(file_recovery->extension); - @ requires \valid(file_recovery->file_stat); - @ requires \valid(file_recovery->file_stat->file_hint); - @ requires valid_read_string(file_recovery->file_stat->file_hint->description); + @ requires valid_file_recovery(file_recovery); @ requires \valid(params); @ requires \valid(params->disk); @ requires \valid_read(options); @ requires \valid(list_search_space); - @ requires \valid(buffer + (0 .. params->blocksize -1)); + @ requires \valid_read(buffer + (0 .. params->blocksize -1)); @ requires params->disk->sector_size > 0; + @ requires \separated(file_recovery_new, file_recovery, params, options, list_search_space, buffer+(..), file_recovered, &errno); @ ensures \result == PSTATUS_OK || \result == PSTATUS_EACCES; - @ ensures *file_recovered == PFSTATUS_BAD || *file_recovered == PFSTATUS_OK || *file_recovered == PFSTATUS_OK_TRUNCATED; @*/ +// ensures *file_recovered == PFSTATUS_BAD || *file_recovered == PFSTATUS_OK || *file_recovered == PFSTATUS_OK_TRUNCATED; static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new, file_recovery_t *file_recovery, struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space, const unsigned char *buffer, pfstatus_t *file_recovered, const uint64_t offset) { *file_recovered=PFSTATUS_BAD; @@ -97,13 +101,17 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new, return PSTATUS_OK; if(file_recovery->file_stat!=NULL) { + /*@ assert valid_file_stat(file_recovery->file_stat); */ +#ifndef __FRAMAC__ if(options->verbose > 1) log_trace("A known header has been found, recovery of the previous file is finished\n"); +#endif *file_recovered=file_finish2(file_recovery, params, options->paranoid, list_search_space); if(*file_recovered==PFSTATUS_OK_TRUNCATED) return PSTATUS_OK; } file_recovery_cpy(file_recovery, file_recovery_new); +#ifndef __FRAMAC__ if(options->verbose > 1) { log_info("%s header found at sector %lu\n", @@ -113,12 +121,15 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new, log_info("file_recovery->location.start=%lu\n", (unsigned long)(file_recovery->location.start/params->disk->sector_size)); } +#endif +#ifndef __FRAMAC__ if(file_recovery->file_stat->file_hint==&file_hint_dir && options->verbose > 0) { /* FAT directory found, list the file */ const unsigned int blocksize=params->blocksize; const unsigned int read_size=(blocksize>65536?blocksize:65536); photorec_dir_fat(buffer, read_size, file_recovery->location.start/params->disk->sector_size); } +#endif set_filename(file_recovery, params); if(file_recovery->file_stat->file_hint->recover==1) { @@ -129,7 +140,9 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new, #endif if(!file_recovery->handle) { +#ifndef __FRAMAC__ log_critical("Cannot create file %s: %s\n", file_recovery->filename, strerror(errno)); +#endif params->offset=offset; return PSTATUS_EACCES; } @@ -137,26 +150,43 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new, return PSTATUS_OK; } +/*@ + @ requires \valid(file_recovery); + @ requires valid_file_recovery(file_recovery); + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \valid_read(options); + @ requires valid_list_search_space(list_search_space); + @ requires \valid_read(buffer + (0 .. params->blocksize -1)); + @ requires \valid(file_recovered); + @ requires \separated(file_recovery, params, options, list_search_space, buffer, file_recovered); + @ ensures valid_file_recovery(file_recovery); + @*/ +// ensures valid_list_search_space(list_search_space); inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space, const unsigned char *buffer, pfstatus_t *file_recovered, const uint64_t offset) { const struct td_list_head *tmpl; const unsigned int blocksize=params->blocksize; const unsigned int read_size=(blocksize>65536?blocksize:65536); file_recovery_t file_recovery_new; + /*@ assert valid_file_recovery(file_recovery); */ file_recovery_new.blocksize=blocksize; file_recovery_new.location.start=offset; if(file_recovery->file_stat!=NULL && file_recovery->file_stat->file_hint==&file_hint_tar && is_valid_tar_header((const struct tar_posix_header *)(buffer-0x200))) { /* Currently saving a tar, do not check the data for know header */ +#ifndef __FRAMAC__ if(options->verbose > 1) { log_verbose("Currently saving a tar file, sector %lu.\n", (unsigned long)((offset-params->partition->part_offset)/params->disk->sector_size)); } +#endif return PSTATUS_OK; } file_recovery_new.file_stat=NULL; file_recovery_new.location.start=offset; + /*@ loop invariant valid_file_recovery(file_recovery); */ td_list_for_each(tmpl, &file_check_list.list) { const struct td_list_head *tmp; @@ -164,10 +194,13 @@ inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, st td_list_for_each(tmp, &pos->file_checks[buffer[pos->offset]].list) { const file_check_t *file_check=td_list_entry_const(tmp, const file_check_t, list); + /*@ assert \valid_function(file_check->header_check); */ + /*@ assert valid_file_check_node(file_check); */ if((file_check->length==0 || memcmp(buffer + file_check->offset, file_check->value, file_check->length)==0) && file_check->header_check(buffer, read_size, 0, file_recovery, &file_recovery_new)!=0) { file_recovery_new.file_stat=file_check->file_stat; + /*@ assert valid_file_recovery(&file_recovery_new); */ return photorec_header_found(&file_recovery_new, file_recovery, params, options, list_search_space, buffer, file_recovered, offset); } } diff --git a/src/phrecn.h b/src/phrecn.h index 598fa1b4..61df09e6 100644 --- a/src/phrecn.h +++ b/src/phrecn.h @@ -25,6 +25,15 @@ extern "C" { #endif +/*@ + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \valid_read(options); + @ requires \valid(list_search_space); + @ requires \separated(params, options, list_search_space); + @ requires params->cmd_run == \null || valid_read_string(params->cmd_run); + @ requires valid_read_string(params->recup_dir); + @*/ int photorec(struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space); #ifdef HAVE_NCURSES void interface_file_select_ncurses(file_enable_t *files_enable); diff --git a/src/pnext.h b/src/pnext.h index b2196211..862bee1c 100644 --- a/src/pnext.h +++ b/src/pnext.h @@ -23,6 +23,13 @@ #define _PNEXT_H /* #define DEBUG_GET_NEXT_SECTOR */ +/*@ + @ requires \valid_read(list_search_space); + @ requires \valid(current_search_space); + @ requires \valid(offset); + @ requires \separated(list_search_space, current_search_space, offset); + @ assigns *current_search_space, *offset; + @*/ static #ifndef DEBUG_GET_NEXT_SECTOR inline @@ -40,6 +47,13 @@ void get_next_header(const alloc_data_t *list_search_space, alloc_data_t **curre *offset=(*current_search_space)->start; } +/*@ + @ requires \valid_read(list_search_space); + @ requires \valid(current_search_space); + @ requires \valid(offset); + @ requires \separated(list_search_space, current_search_space, offset); + @ assigns *current_search_space, *offset; + @*/ static #ifndef DEBUG_GET_NEXT_SECTOR inline @@ -74,6 +88,13 @@ void get_next_sector(const alloc_data_t *list_search_space, alloc_data_t **curre get_next_header(list_search_space, current_search_space, offset); } +/*@ + @ requires \valid_read(list_search_space); + @ requires \valid(current_search_space); + @ requires \valid(offset); + @ requires \separated(list_search_space, current_search_space, offset); + @ assigns *current_search_space, *offset; + @*/ static inline void get_prev_header(const alloc_data_t *list_search_space, alloc_data_t **current_search_space, uint64_t *offset, const unsigned int blocksize) { if((*current_search_space) != list_search_space) @@ -81,6 +102,13 @@ static inline void get_prev_header(const alloc_data_t *list_search_space, alloc_ *offset=(*current_search_space)->end + 1 - blocksize; } +/*@ + @ requires \valid_read(list_search_space); + @ requires \valid(current_search_space); + @ requires \valid(offset); + @ requires \separated(list_search_space, current_search_space, offset); + @ assigns *current_search_space, *offset; + @*/ static inline void get_prev_sector(const alloc_data_t *list_search_space, alloc_data_t **current_search_space, uint64_t *offset, const unsigned int blocksize) { if((*current_search_space) == list_search_space) diff --git a/src/ppartseln.h b/src/ppartseln.h index 85869196..a1b8f3c6 100644 --- a/src/ppartseln.h +++ b/src/ppartseln.h @@ -25,6 +25,16 @@ extern "C" { #endif +/*@ + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \valid(options); + @ requires \valid(list_search_space); + @ requires params->cmd_run == \null || valid_read_string(params->cmd_run); + @ requires \valid_function(params->disk->description); + @ requires \separated(params, options, list_search_space); + @ */ +// ensures params->cmd_run == \null || valid_read_string(params->cmd_run); void menu_photorec(struct ph_param *params, struct ph_options *options, alloc_data_t*list_search_space); #ifdef __cplusplus diff --git a/src/psearch.h b/src/psearch.h index fb4c7f39..6105e229 100644 --- a/src/psearch.h +++ b/src/psearch.h @@ -22,6 +22,9 @@ #ifndef _PSEARCH_H #define _PSEARCH_H +/*@ + @ requires \valid(data); + @*/ static inline alloc_data_t *file_add_data(alloc_data_t *data, const uint64_t offset, const unsigned int content) { if(!(data->start <= offset && offset <= data->end)) @@ -48,6 +51,12 @@ static inline alloc_data_t *file_add_data(alloc_data_t *data, const uint64_t off } } +/*@ + @ requires \valid(dst); + @ requires \valid_read(src); + @ requires \separated(dst, src); + @*/ +// assigns *dst; static inline void file_recovery_cpy(file_recovery_t *dst, const file_recovery_t *src) { memcpy(dst, src, sizeof(*dst)); @@ -56,6 +65,11 @@ static inline void file_recovery_cpy(file_recovery_t *dst, const file_recovery_t } /* Check if the block looks like an indirect/double-indirect block */ +/*@ + @ requires blocksize >= 8; + @ requires \valid_read(buffer + (0 .. blocksize-1)); + @ assigns \result; + @*/ static inline int ind_block(const unsigned char *buffer, const unsigned int blocksize) { const uint32_t *p32=(const uint32_t *)buffer; @@ -65,6 +79,9 @@ static inline int ind_block(const unsigned char *buffer, const unsigned int bloc return 0; if(le32(p32[1])==le32(p32[0])+blocksize/4+1) diff=blocksize/4+1; /* DIND: Double Indirect block */ + /*@ + @ loop assigns i; + @*/ for(i=0;istatus==STATUS_QUIT) @@ -195,6 +197,9 @@ int session_save(alloc_data_t *list_free_space, struct ph_param *params, const if(params->blocksize>0) fprintf(f_session,"blocksize,%u,", params->blocksize); fprintf(f_session,"fileopt,"); + /*@ + @ loop assigns i, disable, enable, enable_by_default; + @*/ for(i=0;files_enable[i].file_hint!=NULL;i++) { if(files_enable[i].enable==0) @@ -296,7 +301,7 @@ int session_save(alloc_data_t *list_free_space, struct ph_param *params, const case STATUS_QUIT: break; } - if(params->status!=STATUS_FIND_OFFSET && params->offset!=-1) + if(params->status!=STATUS_FIND_OFFSET && params->offset!=PH_INVALID_OFFSET) fprintf(f_session, "%llu,", (long long unsigned)(params->offset/params->disk->sector_size)); fprintf(f_session,"inter\n"); diff --git a/src/sessionp.h b/src/sessionp.h index 18ab7324..c5a1b57f 100644 --- a/src/sessionp.h +++ b/src/sessionp.h @@ -25,8 +25,29 @@ extern "C" { #endif +/*@ + @ requires \valid(cmd_device); + @ requires \valid(current_cmd); + @ requires valid_list_search_space(list_free_space); + @ requires \separated(cmd_device, current_cmd, list_free_space); + @*/ +// ensures *cmd_device==\null || valid_read_string(*cmd_device); +// ensures *current_cmd==\null || valid_read_string(*current_cmd); +// ensures valid_list_search_space(list_free_space); int session_load(char **cmd_device, char **current_cmd, alloc_data_t *list_free_space); -int session_save(alloc_data_t *list_free_space, struct ph_param *params, const struct ph_options *options); + +/*@ + @ requires list_free_space==\null || \valid_read(list_free_space); + @ requires params==\null || \valid_read(params); + @ requires options==\null || \valid_read(options); + @*/ +int session_save(const alloc_data_t *list_free_space, const struct ph_param *params, const struct ph_options *options); + +/*@ + @ requires \valid_read(list_free_space); + @ requires params==\null || \valid_read(params); + @ requires options==\null || \valid_read(options); + @*/ time_t regular_session_save(alloc_data_t *list_free_space, struct ph_param *params, const struct ph_options *options, time_t current_time); #ifdef __cplusplus diff --git a/src/setdate.h b/src/setdate.h index 0a4d3b81..ea76f4d1 100644 --- a/src/setdate.h +++ b/src/setdate.h @@ -24,6 +24,11 @@ #ifdef __cplusplus extern "C" { #endif + +/*@ + @ requires valid_read_string(pathname); + @ assigns \nothing; + @*/ int set_date(const char *pathname, time_t actime, time_t modtime); #ifdef __cplusplus } /* closing brace for extern "C" */ diff --git a/src/tanalyse.c b/src/tanalyse.c index 8732c42d..48de06d2 100644 --- a/src/tanalyse.c +++ b/src/tanalyse.c @@ -62,6 +62,7 @@ static list_part_t *interface_analyse_ncurses(disk_t *disk_car, const int verbos wrefresh(stdscr); #endif list_part=disk_car->arch->read_part(disk_car,verbose,saveheader); + /*@ assert valid_list_part(list_part); */ log_info("Current partition structure:\n"); screen_buffer_to_log(); #ifdef HAVE_NCURSES diff --git a/src/tanalyse.h b/src/tanalyse.h index cef8b9eb..94733be8 100644 --- a/src/tanalyse.h +++ b/src/tanalyse.h @@ -25,6 +25,10 @@ extern "C" { #endif +/*@ + @ requires valid_disk(disk_car); + @ ensures valid_list_part(\result); + @*/ list_part_t *interface_analyse(disk_t *disk_car, const int verbose, const int saveheader, char**current_cmd); #ifdef __cplusplus diff --git a/src/tload.h b/src/tload.h index f098fa03..aeaeec30 100644 --- a/src/tload.h +++ b/src/tload.h @@ -26,6 +26,10 @@ extern "C" { #endif +/*@ + @ requires valid_disk(disk_car); + @ requires valid_list_part(list_part); + @*/ list_part_t *interface_load(disk_t *disk_car,list_part_t *list_part, const int verbose); #ifdef __cplusplus diff --git a/src/tpartwr.h b/src/tpartwr.h index b12187fc..f92d3ea7 100644 --- a/src/tpartwr.h +++ b/src/tpartwr.h @@ -25,6 +25,10 @@ extern "C" { #endif +/*@ + @ requires valid_disk(disk_car); + @ requires valid_list_part(list_part); + @*/ int interface_write(disk_t *disk_car,list_part_t *list_part,const int can_search_deeper, const int can_ask_minmax_ext, int *no_confirm, char **current_cmd, unsigned int *menu); #ifdef __cplusplus diff --git a/src/unicode.h b/src/unicode.h index 60fecca0..22d2ccff 100644 --- a/src/unicode.h +++ b/src/unicode.h @@ -25,7 +25,18 @@ extern "C" { #endif +/*@ + @ requires \valid(to + ( 0 .. len-1)); + @ requires \valid_read(from + ( 0 .. len-1)); + @ requires \separated(to + (..), from + (..)); + @*/ int UCSle2str(char *to, const uint16_t *from, const unsigned int len); + +/*@ + @ requires \valid(to + ( 0 .. len-1)); + @ requires \valid_read(from + ( 0 .. len-1)); + @ requires \separated(to + (..), from + (..)); + @*/ int str2UCSle(uint16_t *to, const char *from, const unsigned int len); #ifdef __cplusplus