From 4e44db2b463e4b1ad94a064bd69f999e93443a95 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Thu, 14 Jul 2022 10:09:09 +0200 Subject: [PATCH] Improve Frama-C annotations --- src/alignio.h | 2 ++ src/analyse.h | 12 ++++++++++++ src/apfs.h | 1 + src/bfs.h | 1 + src/bsd.h | 1 + src/btrfs.h | 1 + src/chgtype.h | 1 + src/cramfs.h | 1 + src/exfat.h | 2 ++ src/exfatp.h | 1 + src/ext2.h | 1 + src/ext2grp.h | 2 ++ src/f2fs.h | 1 + src/fat.h | 6 ++++++ src/fat_cluster.h | 1 + src/fat_dir.h | 1 + src/fatp.c | 3 +++ src/fatp.h | 1 + src/filegen.h | 2 ++ src/gfs2.h | 1 + src/hdaccess.h | 6 +++--- src/hfs.h | 1 + src/hfsp.h | 2 ++ src/hpfs.h | 1 + src/io_redir.c | 2 ++ src/iso.h | 1 + src/jfs.h | 1 + src/list_sort.c | 6 ++++++ src/luks.h | 1 + src/netware.h | 1 + src/ntfs.c | 33 ++++++++++++++++++++++++--------- src/ntfs.h | 1 + src/partauto.h | 1 + src/pdisksel.c | 3 ++- src/pdisksel.h | 5 ++--- src/pdiskseln.h | 2 +- src/photorec.h | 12 ++++++++++++ src/photorec_check_header.h | 11 ++++++++++- src/poptions.h | 1 + src/refs.h | 3 +++ src/rfs.h | 1 + src/savehdr.h | 3 +++ src/sessionp.h | 8 +++++--- src/sun.h | 1 + src/swap.h | 1 + src/sysv.h | 3 +++ src/ufs.h | 1 + src/vmfs.h | 3 +++ src/xfs.h | 1 + src/zfs.h | 1 + 50 files changed, 138 insertions(+), 21 deletions(-) diff --git a/src/alignio.h b/src/alignio.h index be949e26..cc4d6b0f 100644 --- a/src/alignio.h +++ b/src/alignio.h @@ -33,6 +33,7 @@ @ requires offset < 0x8000000000000000; @ requires \valid((char *)buf + (0 .. count -1)); @ requires \separated(disk_car, (char *)buf); + @ decreases 0; @ ensures valid_disk(disk_car); @*/ static int align_pread(int (*fnct_pread)(const disk_t *disk_car, void *buf, const unsigned int count, const uint64_t offset), @@ -90,6 +91,7 @@ static int align_pread(int (*fnct_pread)(const disk_t *disk_car, void *buf, cons @ requires offset < 0x8000000000000000; @ requires \valid_read((char *)buf + (0 .. count -1)); @ requires \separated(disk_car, (char *)buf); + @ decreases 0; @ 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), diff --git a/src/analyse.h b/src/analyse.h index 6b3f3836..047ccbb6 100644 --- a/src/analyse.h +++ b/src/analyse.h @@ -31,6 +31,7 @@ extern "C" { @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_type_0(const unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind); @@ -40,6 +41,7 @@ int search_type_0(const unsigned char *buffer, disk_t *disk_car,partition_t *par @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_type_1(const unsigned char *buffer, const disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind); @@ -49,6 +51,7 @@ int search_type_1(const unsigned char *buffer, const disk_t *disk_car, partition @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_type_2(const unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind); @@ -58,6 +61,7 @@ int search_type_2(const unsigned char *buffer, disk_t *disk_car,partition_t *par @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_type_8(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind); @@ -67,6 +71,7 @@ int search_type_8(unsigned char *buffer, disk_t *disk_car,partition_t *partition @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_type_16(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind); @@ -76,6 +81,7 @@ int search_type_16(unsigned char *buffer, disk_t *disk_car,partition_t *partitio @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_type_64(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind); @@ -85,6 +91,7 @@ int search_type_64(unsigned char *buffer, disk_t *disk_car,partition_t *partitio @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_type_128(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind); @@ -94,6 +101,7 @@ int search_type_128(unsigned char *buffer, disk_t *disk_car,partition_t *partiti @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_type_2048(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind); @@ -103,6 +111,7 @@ int search_type_2048(unsigned char *buffer, disk_t *disk_car,partition_t *partit @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk, partition); + @ decreases 0; @*/ int search_exFAT_backup(unsigned char *buffer, disk_t *disk, partition_t *partition); @@ -112,6 +121,7 @@ int search_exFAT_backup(unsigned char *buffer, disk_t *disk, partition_t *partit @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_FAT_backup(unsigned char *buffer, disk_t *disk_car,partition_t *partition, const int verbose, const int dump_ind); @@ -121,6 +131,7 @@ int search_FAT_backup(unsigned char *buffer, disk_t *disk_car,partition_t *parti @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_HFS_backup(unsigned char *buffer, disk_t *disk_car,partition_t *partition, const int verbose, const int dump_ind); @@ -130,6 +141,7 @@ int search_HFS_backup(unsigned char *buffer, disk_t *disk_car,partition_t *parti @ requires \valid(partition); @ requires valid_partition(partition); @ requires \separated(buffer, disk_car, partition); + @ decreases 0; @*/ int search_NTFS_backup(unsigned char *buffer, disk_t *disk_car,partition_t *partition, const int verbose, const int dump_ind); diff --git a/src/apfs.h b/src/apfs.h index b9163c4f..a9932e88 100644 --- a/src/apfs.h +++ b/src/apfs.h @@ -30,6 +30,7 @@ extern "C" { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires \separated(disk_car, partition); + @ decreases 0; @*/ int check_APFS(disk_t *disk_car, partition_t *partition); diff --git a/src/bfs.h b/src/bfs.h index fb3dd7d0..d1a3b0d9 100644 --- a/src/bfs.h +++ b/src/bfs.h @@ -90,6 +90,7 @@ struct disk_super_block /* super block as it is on disk */ @ requires \valid(partition); @ requires valid_disk(disk_car); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_BeFS(disk_t *disk_car, partition_t *partition); diff --git a/src/bsd.h b/src/bsd.h index 52c9f02c..82c4746d 100644 --- a/src/bsd.h +++ b/src/bsd.h @@ -174,6 +174,7 @@ struct disklabel { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_BSD(disk_t *disk_car, partition_t *partition, const int verbose, const unsigned int max_partitions); diff --git a/src/btrfs.h b/src/btrfs.h index 022c6962..d916f593 100644 --- a/src/btrfs.h +++ b/src/btrfs.h @@ -145,6 +145,7 @@ struct btrfs_super_block { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires \separated(disk_car, partition); + @ decreases 0; @*/ int check_btrfs(disk_t *disk_car, partition_t *partition); diff --git a/src/chgtype.h b/src/chgtype.h index 3365eb51..3308a0d5 100644 --- a/src/chgtype.h +++ b/src/chgtype.h @@ -32,6 +32,7 @@ extern "C" { @ requires valid_partition(partition); @ requires \valid(current_cmd); @ requires \separated(disk_car, partition, current_cmd); + @ decreases 0; @*/ void change_part_type_cli(const disk_t *disk_car,partition_t *partition, char **current_cmd); diff --git a/src/cramfs.h b/src/cramfs.h index eef22aae..695f4072 100644 --- a/src/cramfs.h +++ b/src/cramfs.h @@ -89,6 +89,7 @@ struct cramfs_super { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires \separated(disk_car, partition); + @ decreases 0; @*/ int check_cramfs(disk_t *disk_car,partition_t *partition,const int verbose); diff --git a/src/exfat.h b/src/exfat.h index 29e0eee1..54ae4d80 100644 --- a/src/exfat.h +++ b/src/exfat.h @@ -106,6 +106,7 @@ uint64_t exfat_cluster_to_offset(const struct exfat_super_block *exfat_header, c @ requires \valid_read(partition); @ requires \valid_read(exfat_header); @ requires \separated(disk, partition, exfat_header, (char *)buffer); + @ decreases 0; @*/ int exfat_read_cluster(disk_t *disk, const partition_t *partition, const struct exfat_super_block*exfat_header, void *buffer, const unsigned int cluster); @@ -114,6 +115,7 @@ int exfat_read_cluster(disk_t *disk, const partition_t *partition, const struct @ requires valid_disk(disk); @ requires \valid(partition); @ requires \separated(disk, partition); + @ decreases 0; @*/ int check_exFAT(disk_t *disk, partition_t *partition); diff --git a/src/exfatp.h b/src/exfatp.h index f31d323a..f14d28ac 100644 --- a/src/exfatp.h +++ b/src/exfatp.h @@ -32,6 +32,7 @@ extern "C" { @ requires valid_partition(partition); @ requires valid_list_search_space(list_search_space); @ requires \separated(disk, partition, list_search_space); + @ decreases 0; @*/ // ensures valid_list_search_space(list_search_space); unsigned int exfat_remove_used_space(disk_t *disk, const partition_t *partition, alloc_data_t *list_search_space); diff --git a/src/ext2.h b/src/ext2.h index bee4d595..dbf8ed8e 100644 --- a/src/ext2.h +++ b/src/ext2.h @@ -30,6 +30,7 @@ extern "C" { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires \separated(disk_car, partition); + @ decreases 0; @*/ int check_EXT2(disk_t *disk_car, partition_t *partition, const int verbose); diff --git a/src/ext2grp.h b/src/ext2grp.h index 231db84d..96f4f886 100644 --- a/src/ext2grp.h +++ b/src/ext2grp.h @@ -32,6 +32,7 @@ extern "C" { @ requires \valid(disk); @ requires \valid_read(partition); @ requires \separated(list_search_space, disk, partition); + @ decreases 0; @ ensures valid_disk(disk); @*/ // ensures valid_list_search_space(list_search_space); @@ -45,6 +46,7 @@ unsigned int ext2_fix_group(alloc_data_t *list_search_space, disk_t *disk, const @ requires \valid(disk); @ requires \valid_read(partition); @ requires \separated(list_search_space, disk, partition); + @ decreases 0; @ ensures valid_disk(disk); @*/ // ensures valid_list_search_space(list_search_space); diff --git a/src/f2fs.h b/src/f2fs.h index 46949bfd..312799a7 100644 --- a/src/f2fs.h +++ b/src/f2fs.h @@ -30,6 +30,7 @@ extern "C" { @ requires valid_disk(disk); @ requires \valid(partition); @ requires \separated(disk, partition); + @ decreases 0; @*/ int check_f2fs(disk_t *disk, partition_t *partition); diff --git a/src/fat.h b/src/fat.h index 04603de7..61924bac 100644 --- a/src/fat.h +++ b/src/fat.h @@ -33,6 +33,7 @@ extern "C" { @ requires \valid_read(partition); @ requires valid_partition(partition); @ requires separation: \separated(disk, partition); + @ decreases 0; @*/ int comp_FAT(disk_t *disk, const partition_t *partition, const unsigned long int fat_size, const unsigned long int sect_res); @@ -57,6 +58,7 @@ unsigned int get_next_cluster(disk_t *disk, const partition_t *partition, const @ requires \valid_read(partition); @ requires valid_partition(partition); @ requires separation: \separated(disk, partition); + @ decreases 0; @*/ int set_next_cluster(disk_t *disk, const partition_t *partition, const upart_type_t upart_type, const int offset, const unsigned int cluster, const unsigned int next_cluster); @@ -96,6 +98,7 @@ int is_part_fat32(const partition_t *partition); @ requires \valid_read(partition); @ requires valid_partition(partition); @ requires separation: \separated(disk, partition); + @ decreases 0; @*/ unsigned int fat32_get_prev_cluster(disk_t *disk, const partition_t *partition, const unsigned int fat_offset, const unsigned int cluster, const unsigned int no_of_cluster); @@ -107,6 +110,7 @@ unsigned int fat32_get_prev_cluster(disk_t *disk, const partition_t *partition, @ requires separation: \separated(disk, partition); @ requires \valid(next_free); @ requires \valid(free_count); + @ decreases 0; @*/ int fat32_free_info(disk_t *disk, const partition_t *partition, const unsigned int fat_offset, const unsigned int no_of_cluster, unsigned int *next_free, unsigned int *free_count); @@ -138,6 +142,7 @@ int recover_FAT(disk_t *disk, const struct fat_boot_sector*fat_header, partition @ requires \valid(partition); @ requires valid_partition(partition); @ requires separation: \separated(disk, partition); + @ decreases 0; @*/ int check_FAT(disk_t *disk, partition_t *partition, const int verbose); @@ -167,6 +172,7 @@ int recover_OS2MB(const disk_t *disk, const struct fat_boot_sector*fat_header, p @ requires \valid(partition); @ requires valid_partition(partition); @ requires separation: \separated(disk, partition); + @ decreases 0; @*/ int check_OS2MB(disk_t *disk, partition_t *partition, const int verbose); diff --git a/src/fat_cluster.h b/src/fat_cluster.h index df818a66..aeb3bba8 100644 --- a/src/fat_cluster.h +++ b/src/fat_cluster.h @@ -50,6 +50,7 @@ struct cluster_offset_struct @ requires \valid(sectors_per_cluster); @ requires \valid(offset); @ requires \separated(disk_car, partition, sectors_per_cluster, offset); + @ decreases 0; @*/ int find_sectors_per_cluster(disk_t *disk_car, const partition_t *partition, const int verbose, const int dump_ind, unsigned int *sectors_per_cluster, uint64_t *offset, const upart_type_t upart_type); diff --git a/src/fat_dir.h b/src/fat_dir.h index 9e1d34a5..8028500d 100644 --- a/src/fat_dir.h +++ b/src/fat_dir.h @@ -41,6 +41,7 @@ int dir_fat_aux(const unsigned char*buffer, const unsigned int size, const unsig @ requires valid_partition(partition); @ requires \valid(dir_data); @ requires \separated(disk_car, partition, dir_data); + @ decreases 0; @*/ dir_partition_t dir_partition_fat_init(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const int verbose); diff --git a/src/fatp.c b/src/fatp.c index a227082e..a98f13a6 100644 --- a/src/fatp.c +++ b/src/fatp.c @@ -44,6 +44,7 @@ @ requires valid_partition(partition); @ requires \valid(list_search_space); @ requires \separated(disk, partition, list_search_space); + @ decreases 0; @*/ 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) { @@ -101,6 +102,7 @@ static void fat12_remove_used_space(disk_t *disk,const partition_t *partition, a @ requires valid_partition(partition); @ requires \valid(list_search_space); @ requires \separated(disk_car, partition, list_search_space); + @ decreases 0; @*/ 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) { @@ -153,6 +155,7 @@ static void fat16_remove_used_space(disk_t *disk_car,const partition_t *partitio @ requires valid_partition(partition); @ requires \valid(list_search_space); @ requires \separated(disk_car, partition, list_search_space); + @ decreases 0; @*/ 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) { diff --git a/src/fatp.h b/src/fatp.h index 699a25e3..745ee827 100644 --- a/src/fatp.h +++ b/src/fatp.h @@ -32,6 +32,7 @@ extern "C" { @ requires valid_partition(partition); @ requires valid_list_search_space(list_search_space); @ requires \separated(disk_car, partition, list_search_space); + @ decreases 0; @*/ // 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); diff --git a/src/filegen.h b/src/filegen.h index 4fbbcf5f..2051b882 100644 --- a/src/filegen.h +++ b/src/filegen.h @@ -356,6 +356,7 @@ void register_header_check(const unsigned int offset, const void *value, const u /*@ @ requires \valid(files_enable); + @ decreases 0; @*/ file_stat_t * init_file_stats(file_enable_t *files_enable); @@ -393,6 +394,7 @@ void header_ignored(const file_recovery_t *file_recovery_new); @ requires \valid_function(file_recovery->file_check); @ requires \initialized(&file_recovery->file_check); @ requires \initialized(&file_recovery->handle); + @ decreases 0; @ ensures \result == 0 || \result == 1; @*/ // ensures valid_file_recovery(file_recovery); diff --git a/src/gfs2.h b/src/gfs2.h index b3a7af05..9d0941bf 100644 --- a/src/gfs2.h +++ b/src/gfs2.h @@ -84,6 +84,7 @@ struct gfs2_sb { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires \separated(disk_car, partition); + @ decreases 0; @*/ int check_gfs2(disk_t *disk_car, partition_t *partition); diff --git a/src/hdaccess.h b/src/hdaccess.h index 81d1c011..6cd2938f 100644 --- a/src/hdaccess.h +++ b/src/hdaccess.h @@ -30,12 +30,13 @@ extern "C" { @ requires disk_car->sector_size > 0; @ requires disk_car->geom.heads_per_cylinder > 0; @ requires \valid_function(disk_car->pread); + @ decreases 0; @ ensures valid_disk(disk_car); @*/ void hd_update_geometry(disk_t *disk_car, const int verbose); /*@ - @ requires list_disk==\null || \valid_read(list_disk); + @ requires valid_list_disk(list_disk); @*/ void hd_update_all_geometry(const list_disk_t * list_disk, const int verbose); @@ -47,11 +48,10 @@ list_disk_t *hd_parse(list_disk_t *list_disk, const int verbose, const int testd /*@ @ requires valid_read_string(device); - @ 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); + @ ensures \result==\null || valid_disk(\result); @*/ disk_t *file_test_availability(const char *device, const int verbose, const int testdisk_mode); diff --git a/src/hfs.h b/src/hfs.h index cc500d2f..6448fe1e 100644 --- a/src/hfs.h +++ b/src/hfs.h @@ -81,6 +81,7 @@ struct hfs_mdb { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_HFS(disk_t *disk_car, partition_t *partition, const int verbose); diff --git a/src/hfsp.h b/src/hfsp.h index a961904b..d42543ad 100644 --- a/src/hfsp.h +++ b/src/hfsp.h @@ -30,6 +30,7 @@ extern "C" { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires \separated(disk_car, partition); + @ decreases 0; @*/ int check_HFSP(disk_t *disk_car, partition_t *partition, const int verbose); @@ -48,6 +49,7 @@ int test_HFSP(const disk_t *disk_car, const struct hfsp_vh *vh, const partition_ @ requires \valid_read(vh); @ requires \valid(partition); @ requires \separated(disk_car, vh, partition); + @ decreases 0; @*/ int recover_HFSP(disk_t *disk_car, const struct hfsp_vh *vh, partition_t *partition, const int verbose, const int dump_ind, const int backup); diff --git a/src/hpfs.h b/src/hpfs.h index 0e950801..bbcc0c45 100644 --- a/src/hpfs.h +++ b/src/hpfs.h @@ -40,6 +40,7 @@ int recover_HPFS(const disk_t *disk_car, const struct fat_boot_sector *hpfs_head @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires \separated(disk_car, partition); + @ decreases 0; @*/ int check_HPFS(disk_t *disk_car,partition_t *partition, const int verbose); diff --git a/src/io_redir.c b/src/io_redir.c index 5fa867a9..9b09af7c 100644 --- a/src/io_redir.c +++ b/src/io_redir.c @@ -60,12 +60,14 @@ struct info_io_redir @ requires valid_disk(disk_car); @ requires \valid((char *)buffer + (0 .. count-1)); @ requires separation: \separated(disk_car, (char *)buffer + (0 .. count-1)); + @ decreases 0; @*/ static int io_redir_pread(disk_t *disk_car, void *buffer, const unsigned int count, const uint64_t offset); /*@ @ requires \valid(disk_car); @ requires valid_disk(disk_car); + @ decreases 0; @*/ static void io_redir_clean(disk_t *disk_car); diff --git a/src/iso.h b/src/iso.h index bd3e94ff..63de0017 100644 --- a/src/iso.h +++ b/src/iso.h @@ -31,6 +31,7 @@ extern "C" { @ requires \valid(partition); @ requires valid_partition(partition); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_ISO(disk_t *disk_car, partition_t *partition); diff --git a/src/jfs.h b/src/jfs.h index 55967025..273c2a7a 100644 --- a/src/jfs.h +++ b/src/jfs.h @@ -33,6 +33,7 @@ extern "C" { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_JFS(disk_t *disk_car, partition_t *partition); diff --git a/src/list_sort.c b/src/list_sort.c index 92318a51..1edd7fb8 100644 --- a/src/list_sort.c +++ b/src/list_sort.c @@ -36,6 +36,9 @@ * to chaining of merge() calls: null-terminated, no reserved or * sentinel head node, "prev" links not maintained. */ +/*@ + @ decreases 0; + @*/ static struct td_list_head *merge( int (*cmp)(const struct td_list_head *a, const struct td_list_head *b), struct td_list_head *a, struct td_list_head *b) @@ -64,6 +67,9 @@ static struct td_list_head *merge( * prev-link restoration pass, or maintaining the prev links * throughout. */ +/*@ + @ decreases 0; + @*/ static void merge_and_restore_back_links( int (*cmp)(const struct td_list_head *a, const struct td_list_head *b), struct td_list_head *head, diff --git a/src/luks.h b/src/luks.h index f10c5afb..520721a3 100644 --- a/src/luks.h +++ b/src/luks.h @@ -32,6 +32,7 @@ extern "C" { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires \separated(disk_car, partition); + @ decreases 0; @*/ int check_LUKS(disk_t *disk_car, partition_t *partition); diff --git a/src/netware.h b/src/netware.h index 67b2c4d4..7c31aec8 100644 --- a/src/netware.h +++ b/src/netware.h @@ -39,6 +39,7 @@ struct disk_netware @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_netware(disk_t *disk_car, partition_t *partition); diff --git a/src/ntfs.c b/src/ntfs.c index ec2c8f64..22cb4f16 100644 --- a/src/ntfs.c +++ b/src/ntfs.c @@ -43,10 +43,30 @@ #include "fnctdsk.h" #include "lang.h" #include "log.h" -/* #include "guid_cmp.h" */ -extern const arch_fnct_t arch_i386; +#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386) +extern const arch_fnct_t arch_i386; +#endif + +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid_read(ntfs_header); + @ requires \valid(partition); + @ requires valid_partition(partition); + @ requires \separated(disk_car, ntfs_header, partition); + @*/ static void set_NTFS_info(disk_t *disk_car, const struct ntfs_boot_sector*ntfs_header, partition_t *partition); + +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid(partition); + @ requires valid_partition(partition); + @ requires \valid_read(ntfs_header); + @ requires \separated(disk_car, partition, ntfs_header); + @ decreases 0; + @*/ static void ntfs_get_volume_name(disk_t *disk_car, partition_t *partition, const struct ntfs_boot_sector*ntfs_header); unsigned int ntfs_sector_size(const struct ntfs_boot_sector *ntfs_header) @@ -369,6 +389,7 @@ static void ntfs_get_volume_name(disk_t *disk_car, partition_t *partition, const int is_part_ntfs(const partition_t *partition) { +#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386) if(partition->arch==&arch_i386) { switch(partition->part_type_i386) @@ -380,13 +401,7 @@ int is_part_ntfs(const partition_t *partition) break; } } - /* - else if(partition->arch==&arch_gpt) - { - if(guid_cmp(partition->part_type_gpt,GPT_ENT_TYPE_MS_BASIC_DATA)==0) - return 1; - } - */ +#endif return 0; } diff --git a/src/ntfs.h b/src/ntfs.h index 9a42ba2b..c1b5a243 100644 --- a/src/ntfs.h +++ b/src/ntfs.h @@ -31,6 +31,7 @@ extern "C" { @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires \separated(disk_car, partition); + @ decreases 0; @*/ int check_NTFS(disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind); diff --git a/src/partauto.h b/src/partauto.h index dbd7d7bc..1929c69b 100644 --- a/src/partauto.h +++ b/src/partauto.h @@ -31,6 +31,7 @@ extern "C" { @ requires \valid_read(arch); @ requires valid_disk(disk); @ requires separation: \separated(disk, arch); + @ decreases 0; @ ensures valid_disk(disk); @*/ void autodetect_arch(disk_t *disk, const arch_fnct_t *arch); diff --git a/src/pdisksel.c b/src/pdisksel.c index aa86ab25..8e06b567 100644 --- a/src/pdisksel.c +++ b/src/pdisksel.c @@ -41,7 +41,7 @@ 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 invariant disk==\null || valid_disk(disk); @ loop assigns element_disk, disk; @*/ for(element_disk=list_disk;element_disk!=NULL;element_disk=element_disk->next) @@ -51,6 +51,7 @@ disk_t *photorec_disk_selection_cli(const char *cmd_device, const list_disk_t *l } if(disk==NULL) return NULL; + /*@ assert valid_disk(disk); */ { /* disk sector size is now known, fix the sector ranges */ struct td_list_head *search_walker = NULL; diff --git a/src/pdisksel.h b/src/pdisksel.h index a03ce556..2daadb66 100644 --- a/src/pdisksel.h +++ b/src/pdisksel.h @@ -27,11 +27,10 @@ extern "C" { /*@ @ requires valid_read_string(cmd_device); - @ requires \valid_read(list_disk); - @ requires valid_disk(list_disk->disk); + @ requires valid_list_disk(list_disk); @ requires \valid(list_search_space); @ requires \separated(cmd_device, list_disk, list_search_space); - @ ensures valid_disk(\result); + @ ensures \result==\null || 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); diff --git a/src/pdiskseln.h b/src/pdiskseln.h index a961b470..9609edaa 100644 --- a/src/pdiskseln.h +++ b/src/pdiskseln.h @@ -29,7 +29,7 @@ extern "C" { @ requires \valid(params); @ requires valid_ph_param(params); @ requires \valid(options); - @ requires list_disk == \null || (\valid_read(list_disk) && valid_disk(list_disk->disk)); + @ requires valid_list_disk(list_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; diff --git a/src/photorec.h b/src/photorec.h index 84cbb503..517efdbe 100644 --- a/src/photorec.h +++ b/src/photorec.h @@ -225,6 +225,15 @@ uint64_t set_search_start(struct ph_param *params, alloc_data_t **new_current_se @ requires valid_ph_param(params); @ requires \valid_read(options); @ requires \separated(params, options); + @ requires params->disk->sector_size > 0; + @ requires valid_read_string(params->recup_dir); + @ ensures valid_ph_param(params); + @ ensures params->file_nbr == 0; + @ ensures params->status == STATUS_FIND_OFFSET; + @ ensures params->dir_num == 1; + @ ensures params->offset == PH_INVALID_OFFSET; + @ ensures params->blocksize > 0; + @ ensures valid_read_string(params->recup_dir); @*/ void params_reset(struct ph_param *params, const struct ph_options *options); @@ -238,6 +247,7 @@ const char *status_to_name(const photorec_status_t status); @ requires valid_ph_param(params); @ requires \valid_read(options); @ requires \separated(params, options); + @ ensures valid_ph_param(params); @ assigns params->offset, params->status, params->file_nbr; @*/ void status_inc(struct ph_param *params, const struct ph_options *options); @@ -249,6 +259,7 @@ void status_inc(struct ph_param *params, const struct ph_options *options); @ requires \valid_function(disk->arch->read_part); @ requires \valid_read(options); @ requires \separated(disk, options); + @ decreases 0; @ ensures valid_disk(disk); @*/ // ensures valid_list_part(\result); @@ -276,6 +287,7 @@ void file_block_append(file_recovery_t *file_recovery, alloc_data_t *list_search @ 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)); + @ decreases 0; @*/ // 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); diff --git a/src/photorec_check_header.h b/src/photorec_check_header.h index a13ba3ce..3b375e74 100644 --- a/src/photorec_check_header.h +++ b/src/photorec_check_header.h @@ -24,8 +24,12 @@ #ifdef __cplusplus extern "C" { #endif +#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tar) extern const file_hint_t file_hint_tar; +#endif +#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_dir) extern const file_hint_t file_hint_dir; +#endif extern file_check_list_t file_check_list; #if defined(__CYGWIN__) || defined(__MINGW32__) @@ -122,7 +126,7 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new, (unsigned long)(file_recovery->location.start/params->disk->sector_size)); } #endif -#ifndef __FRAMAC__ +#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_dir) 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; @@ -160,6 +164,7 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new, @ requires \valid_read(buffer + (0 .. params->blocksize -1)); @ requires \valid(file_recovered); @ requires \separated(file_recovery, params, options, list_search_space, buffer, file_recovered); + @ decreases 0; @ ensures valid_file_recovery(file_recovery); @*/ // ensures valid_list_search_space(list_search_space); @@ -172,6 +177,7 @@ inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, st /*@ assert valid_file_recovery(file_recovery); */ file_recovery_new.blocksize=blocksize; file_recovery_new.location.start=offset; +#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tar) 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 */ @@ -182,8 +188,10 @@ inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, st (unsigned long)((offset-params->partition->part_offset)/params->disk->sector_size)); } #endif + /*@ assert valid_file_recovery(file_recovery); */ return PSTATUS_OK; } +#endif file_recovery_new.file_stat=NULL; file_recovery_new.location.start=offset; /*@ loop invariant valid_file_recovery(file_recovery); */ @@ -205,6 +213,7 @@ inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, st } } } + /*@ assert valid_file_recovery(file_recovery); */ return PSTATUS_OK; } #ifdef __cplusplus diff --git a/src/poptions.h b/src/poptions.h index 391a9e08..630d319a 100644 --- a/src/poptions.h +++ b/src/poptions.h @@ -30,6 +30,7 @@ extern "C" { @ requires \valid(current_cmd); @ requires valid_read_string(*current_cmd); @ requires \valid(options); + @ requires \separated(options, current_cmd, *current_cmd); @ ensures valid_read_string(*current_cmd); @ */ void interface_options_photorec_cli(struct ph_options *options, char**current_cmd); diff --git a/src/refs.h b/src/refs.h index 8a7f6ec5..f12ca4ed 100644 --- a/src/refs.h +++ b/src/refs.h @@ -38,6 +38,9 @@ struct ReFS_boot_sector { uint16_t checksum; } __attribute__ ((gcc_struct, __packed__)); +/*@ + @ decreases 0; + @*/ int check_ReFS(disk_t *disk, partition_t *partition); int recover_ReFS(const disk_t *disk, const struct ReFS_boot_sector *refs_header, partition_t *partition); diff --git a/src/rfs.h b/src/rfs.h index 6d47dfdb..87acb614 100644 --- a/src/rfs.h +++ b/src/rfs.h @@ -111,6 +111,7 @@ struct format40_super { @ requires \valid(disk_car); @ requires \valid(partition); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_rfs(disk_t *disk_car, partition_t *partition, const int verbose); diff --git a/src/savehdr.h b/src/savehdr.h index b05504bf..94fe3f1d 100644 --- a/src/savehdr.h +++ b/src/savehdr.h @@ -37,17 +37,20 @@ typedef struct /*@ @ requires valid_disk(disk_car); @ requires valid_partition(partition); + @ decreases 0; @*/ int save_header(disk_t *disk_car, const partition_t *partition, const int verbose); /*@ @ requires valid_disk(disk_car); @ requires valid_list_part(list_part); + @ decreases 0; @*/ int partition_save(disk_t *disk_car, const list_part_t *list_part, const int verbose); /*@ @ requires valid_disk(disk_car); + @ decreases 0; @*/ backup_disk_t *partition_load(const disk_t *disk_car, const int verbose); diff --git a/src/sessionp.h b/src/sessionp.h index c5a1b57f..51f6127e 100644 --- a/src/sessionp.h +++ b/src/sessionp.h @@ -37,9 +37,11 @@ extern "C" { int session_load(char **cmd_device, char **current_cmd, alloc_data_t *list_free_space); /*@ - @ requires list_free_space==\null || \valid_read(list_free_space); - @ requires params==\null || \valid_read(params); - @ requires options==\null || \valid_read(options); + @ requires \valid_read(list_free_space); + @ requires valid_ph_param(params); + @ requires \valid_read(options); + @ requires \separated(list_free_space, params, options); + @ ensures valid_ph_param(params); @*/ int session_save(const alloc_data_t *list_free_space, const struct ph_param *params, const struct ph_options *options); diff --git a/src/sun.h b/src/sun.h index 41784373..f0eba9b2 100644 --- a/src/sun.h +++ b/src/sun.h @@ -91,6 +91,7 @@ int recover_sun_i386(const disk_t *disk_car, const sun_partition_i386 *sunlabel, @ requires \valid(disk_car); @ requires \valid(partition); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_sun_i386(disk_t *disk_car, partition_t *partition, const int verbose); diff --git a/src/swap.h b/src/swap.h index bf675666..a2b5809b 100644 --- a/src/swap.h +++ b/src/swap.h @@ -56,6 +56,7 @@ union swap_header { @ requires \valid(disk_car); @ requires \valid(partition); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_Linux_SWAP(disk_t *disk_car, partition_t *partition); diff --git a/src/sysv.h b/src/sysv.h index 7a2f175e..166dd01f 100644 --- a/src/sysv.h +++ b/src/sysv.h @@ -202,6 +202,9 @@ struct coh_super_block { uint32_t s_unique; /* zero, not used */ }; +/*@ + @ decreases 0; + @*/ int check_sysv(disk_t *disk_car,partition_t *partition,const int verbose); int recover_sysv(const disk_t *disk_car, const struct sysv4_super_block *sbd, partition_t *partition,const int verbose, const int dump_ind); diff --git a/src/ufs.h b/src/ufs.h index 5ddfb755..3c50b1f3 100644 --- a/src/ufs.h +++ b/src/ufs.h @@ -475,6 +475,7 @@ struct ufs_super_block { @ requires \valid(disk_car); @ requires \valid(partition); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_ufs(disk_t *disk_car,partition_t *partition,const int verbose); diff --git a/src/vmfs.h b/src/vmfs.h index 46024a69..9284f690 100644 --- a/src/vmfs.h +++ b/src/vmfs.h @@ -41,6 +41,9 @@ struct vmfs_lvm uint64_t blocks; } __attribute__ ((gcc_struct, __packed__)); +/*@ + @ decreases 0; + @*/ int check_VMFS(disk_t *disk,partition_t *partition); int recover_VMFS(const disk_t *disk, const struct vmfs_volume *sb, partition_t *partition, const int verbose, const int dump_ind); #ifdef __cplusplus diff --git a/src/xfs.h b/src/xfs.h index f55d1498..3b7b5086 100644 --- a/src/xfs.h +++ b/src/xfs.h @@ -38,6 +38,7 @@ extern "C" { @ requires \valid(disk_car); @ requires \valid(partition); @ requires separation: \separated(disk_car, partition); + @ decreases 0; @*/ int check_xfs(disk_t *disk_car, partition_t *partition, const int verbose); diff --git a/src/zfs.h b/src/zfs.h index 0e376305..9c5cfed0 100644 --- a/src/zfs.h +++ b/src/zfs.h @@ -42,6 +42,7 @@ struct vdev_boot_header { @ requires \valid(disk); @ requires \valid(partition); @ requires separation: \separated(disk, partition); + @ decreases 0; @*/ int check_ZFS(disk_t *disk, partition_t *partition);