summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-08-08 12:26:37 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-08-08 12:26:37 +0200
commitd19e5362783d2c1dbc3b6cdf3adde5703cc54176 (patch)
tree64a135f30bc635f4b7fea7ee81e7c41e9e413620
parent7503c141089a5d50d35b3d0ccfbca5c43bf0e8d3 (diff)
Additional frama-c annotations
-rw-r--r--src/addpart.h8
-rw-r--r--src/adv.h10
-rw-r--r--src/askloc.h4
-rw-r--r--src/autoset.h4
-rw-r--r--src/bfs.h13
-rw-r--r--src/bsd.h18
-rw-r--r--src/chgarch.h5
-rw-r--r--src/crc.c1
-rw-r--r--src/crc.h4
-rw-r--r--src/dir.h9
-rw-r--r--src/fat.c15
-rw-r--r--src/fat.h114
-rw-r--r--src/file_dir.c26
-rw-r--r--src/file_tar.c12
-rw-r--r--src/fnctdsk.c28
-rw-r--r--src/fnctdsk.h163
-rw-r--r--src/geometry.c1
-rw-r--r--src/geometry.h21
-rw-r--r--src/guid_cmp.h4
-rw-r--r--src/guid_cpy.h9
-rw-r--r--src/hdaccess.h78
-rw-r--r--src/hdcache.h4
-rw-r--r--src/intrf.c4
-rw-r--r--src/intrf.h11
-rw-r--r--src/iso.h11
-rw-r--r--src/jfs.h14
-rw-r--r--src/lvm.h30
-rw-r--r--src/md.h20
-rw-r--r--src/misc.h5
-rw-r--r--src/netware.h12
-rw-r--r--src/ntfs_utl.c6
-rw-r--r--src/partauto.h5
-rw-r--r--src/partgpt.c2
-rw-r--r--src/partgpt.h15
-rw-r--r--src/parthumax.c1
-rw-r--r--src/parti386.c30
-rw-r--r--src/parti386.h21
-rw-r--r--src/partmac.c57
-rw-r--r--src/partnone.c8
-rw-r--r--src/partsun.c6
-rw-r--r--src/partxbox.c2
-rw-r--r--src/pdiskseln.h8
-rw-r--r--src/phcli.c5
-rw-r--r--src/phcli.h6
-rw-r--r--src/phmain.c1
-rw-r--r--src/photorec.h24
-rw-r--r--src/poptions.c1
-rw-r--r--src/poptions.h10
-rw-r--r--src/rfs.h16
-rw-r--r--src/sun.h16
-rw-r--r--src/swap.h11
-rw-r--r--src/ufs.h15
-rw-r--r--src/xfs.h15
-rw-r--r--src/zfs.h17
54 files changed, 917 insertions, 39 deletions
diff --git a/src/addpart.h b/src/addpart.h
index ab66262..cae5f1c 100644
--- a/src/addpart.h
+++ b/src/addpart.h
@@ -20,4 +20,12 @@
*/
+/*@
+ @ requires \valid(disk);
+ @ requires list_part == \null || \valid_read(list_part);
+ @ requires \valid(current_cmd);
+ @ requires valid_read_string(*current_cmd);
+ @ requires separation: \separated(disk, list_part, current_cmd);
+ @ ensures valid_read_string(*current_cmd);
+ @*/
list_part_t *add_partition_cli(disk_t *disk, list_part_t *list_part, char **current_cmd);
diff --git a/src/adv.h b/src/adv.h
index 339ecf5..b62033e 100644
--- a/src/adv.h
+++ b/src/adv.h
@@ -23,7 +23,17 @@
extern "C" {
#endif
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(current_cmd);
+ @ requires valid_string(*current_cmd);
+ @*/
void interface_adv(disk_t *disk_car, const int verbose,const int dump_ind, const unsigned int expert, char**current_cmd);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
int is_part_linux(const partition_t *partition);
#ifdef __cplusplus
diff --git a/src/askloc.h b/src/askloc.h
index 7671883..5dcc8d4 100644
--- a/src/askloc.h
+++ b/src/askloc.h
@@ -24,6 +24,10 @@ extern "C" {
#endif
char *ask_location(const char*msg, const char *src_dir, const char *dst_org);
+
+/*@
+ @ ensures \result == \null || (\result != \null && \freeable(\result) && valid_string(\result));
+ @*/
char *get_default_location(void);
#ifdef __cplusplus
diff --git a/src/autoset.h b/src/autoset.h
index 8f9e150..a5b4a56 100644
--- a/src/autoset.h
+++ b/src/autoset.h
@@ -19,5 +19,9 @@
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
+/*@
+ @ requires \valid(disk_car);
+ @ assigns disk_car->unit;
+ @*/
void autoset_unit(disk_t *disk_car);
diff --git a/src/bfs.h b/src/bfs.h
index 9e78446..7117d4c 100644
--- a/src/bfs.h
+++ b/src/bfs.h
@@ -82,7 +82,20 @@ struct disk_super_block /* super block as it is on disk */
/* this is stored in the fs_byte_order field... it's kind of dumb */
#define BFS_BIG_ENDIAN 0x42494745 /* BIGE */
/* int test_beos(struct disk_super_block *,partition_t); */
+
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
int check_BeFS(disk_t *disk_car, partition_t *partition);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(beos_block);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, beos_block, partition);
+ @*/
int recover_BeFS(const disk_t *disk_car, const struct disk_super_block *beos_block, partition_t *partition, const int dump_ind);
#ifdef __cplusplus
diff --git a/src/bsd.h b/src/bsd.h
index bd94e54..4554864 100644
--- a/src/bsd.h
+++ b/src/bsd.h
@@ -168,8 +168,22 @@ struct disklabel {
#define TST_FS_VINUM 14 /* Vinum drive */
#define TST_FS_RAID 15 /* RAIDFrame drive */
#define TST_FS_JFS2 21 /* IBM JFS2 */
-int check_BSD(disk_t *disk_car,partition_t *partition,const int verbose,const unsigned int max_partitions);
-int recover_BSD(const disk_t *disk_car, const struct disklabel*bsd_header,partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
+int check_BSD(disk_t *disk_car, partition_t *partition, const int verbose, const unsigned int max_partitions);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(bsd_header);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, bsd_header, partition);
+ @*/
+int recover_BSD(const disk_t *disk_car, const struct disklabel*bsd_header, partition_t *partition, const int verbose, const int dump_ind);
+
#ifdef __cplusplus
} /* closing brace for extern "C" */
#endif
diff --git a/src/chgarch.h b/src/chgarch.h
index 5324933..e1b459e 100644
--- a/src/chgarch.h
+++ b/src/chgarch.h
@@ -24,6 +24,11 @@
extern "C" {
#endif
+/*@
+ @ requires \valid(disk);
+ @ requires current_cmd == \null || valid_read_string(*current_cmd);
+ @ ensures current_cmd == \null || valid_read_string(*current_cmd);
+ @*/
int change_arch_type_cli(disk_t *disk, const int verbose, char**current_cmd);
#ifdef __cplusplus
diff --git a/src/crc.c b/src/crc.c
index 0d1b268..58a01e6 100644
--- a/src/crc.c
+++ b/src/crc.c
@@ -91,6 +91,7 @@ unsigned int get_crc32(const void*buf, const unsigned int len, const uint32_t se
register uint32_t crc32val;
const unsigned char *s=(const unsigned char *)buf;
crc32val = seed;
+ /*@ loop assigns crc32val; */
for (i = 0; i < len; i ++)
{
crc32val = crc32_tab[(crc32val ^ s[i]) & 0xff] ^ (crc32val >> 8);
diff --git a/src/crc.h b/src/crc.h
index 50b6667..b49084b 100644
--- a/src/crc.h
+++ b/src/crc.h
@@ -28,6 +28,10 @@ extern "C" {
uint32_t* make_crc32_table(uint32_t poly);
unsigned int get_crc32_gen(const unsigned char *s, const unsigned int len, const uint32_t seed, const uint32_t *crctab);
#endif
+/*@
+ @ requires \valid_read((const char *)s + (0 .. len-1));
+ @ assigns \nothing;
+ @*/
unsigned int get_crc32(const void *s, const unsigned int len, const uint32_t seed);
#ifdef __cplusplus
diff --git a/src/dir.h b/src/dir.h
index b2d4f7a..0a78ae4 100644
--- a/src/dir.h
+++ b/src/dir.h
@@ -75,8 +75,17 @@ struct dir_data
#define FILE_STATUS_MARKED 2
#define FILE_STATUS_ADS 4
+/*@
+ @ requires \valid(datestr);
+ @*/
int set_datestr(char *datestr, size_t n, const time_t timev);
+
+/*@
+ @ requires \valid_read(dir_data);
+ @ requires \valid_read(dir_list);
+ @*/
int dir_aff_log(const dir_data_t *dir_data, const file_info_t*dir_list);
+
void log_list_file(const disk_t *disk_car, const partition_t *partition, const dir_data_t *dir_data, const file_info_t*list);
unsigned int delete_list_file(file_info_t *list);
int dir_whole_partition_log(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const unsigned long int inode);
diff --git a/src/fat.c b/src/fat.c
index cc41a9e..70c78bf 100644
--- a/src/fat.c
+++ b/src/fat.c
@@ -52,8 +52,23 @@ extern const arch_fnct_t arch_mac;
static int log_fat_info(const struct fat_boot_sector*fh1, const upart_type_t upart_type, const unsigned int sector_size);
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);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
static int is_fat12(const partition_t *partition);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
static int is_fat16(const partition_t *partition);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
static int is_fat32(const partition_t *partition);
static int fat32_set_part_name(disk_t *disk_car, partition_t *partition, const struct fat_boot_sector*fat_header)
diff --git a/src/fat.h b/src/fat.h
index 11d0871..b6a043f 100644
--- a/src/fat.h
+++ b/src/fat.h
@@ -113,21 +113,89 @@ struct msdos_dir_slot {
uint8_t name11_12[4]; /* 1C last 2 characters in name */
};
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(partition);
+ @ requires separation: \separated(disk, partition);
+ @*/
+int comp_FAT(disk_t *disk, const partition_t *partition, const unsigned long int fat_size, const unsigned long int sect_res);
-int comp_FAT(disk_t *disk,const partition_t *partition, const unsigned long int fat_size, const unsigned long int sect_res);
+/*@
+ @ requires \valid_read(fh1);
+ @ requires \valid_read(fh2);
+ @*/
int log_fat2_info(const struct fat_boot_sector*fh1, const struct fat_boot_sector*fh2, const upart_type_t upart_type, const unsigned int sector_size);
-unsigned int get_next_cluster(disk_t *disk,const partition_t *partition, const upart_type_t upart_type,const int offset, const unsigned int cluster);
-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);
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(partition);
+ @ requires separation: \separated(disk, partition);
+ @*/
+unsigned int get_next_cluster(disk_t *disk, const partition_t *partition, const upart_type_t upart_type, const int offset, const unsigned int cluster);
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(partition);
+ @ requires separation: \separated(disk, partition);
+ @*/
+int set_next_cluster(disk_t *disk, const partition_t *partition, const upart_type_t upart_type, const int offset, const unsigned int cluster, const unsigned int next_cluster);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
int is_fat(const partition_t *partition);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
int is_part_fat(const partition_t *partition);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
int is_part_fat12(const partition_t *partition);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
int is_part_fat16(const partition_t *partition);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
int is_part_fat32(const partition_t *partition);
-unsigned int fat32_get_prev_cluster(disk_t *disk,const partition_t *partition, const unsigned int fat_offset, const unsigned int cluster, const unsigned int no_of_cluster);
-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);
+
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(partition);
+ @ requires separation: \separated(disk, partition);
+ @*/
+unsigned int fat32_get_prev_cluster(disk_t *disk, const partition_t *partition, const unsigned int fat_offset, const unsigned int cluster, const unsigned int no_of_cluster);
+
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(partition);
+ @ requires separation: \separated(disk, partition);
+ @ requires \valid(next_free);
+ @ requires \valid(free_count);
+ @*/
+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);
+
+/*@
+ @ requires \valid_read(boot_fat32 + (0 .. sector_size-1));
+ @ assigns \nothing;
+ @*/
unsigned long int fat32_get_free_count(const unsigned char *boot_fat32, const unsigned int sector_size);
+
+/*@
+ @ requires \valid_read(boot_fat32 + (0 .. sector_size-1));
+ @ assigns \nothing;
+ @*/
unsigned long int fat32_get_next_free(const unsigned char *boot_fat32, const unsigned int sector_size);
#define DELETED_FLAG 0xe5 /* marks file as deleted when in name[0] */
@@ -153,11 +221,47 @@ unsigned long int fat32_get_next_free(const unsigned char *boot_fat32, const uns
#define FAT32_EOC 0x0FFFFFF8
#define FAT1x_BOOT_SECTOR_SIZE 0x200
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(fat_header);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk, partition, fat_header);
+ @*/
int recover_FAT(disk_t *disk, const struct fat_boot_sector*fat_header, partition_t *partition, const int verbose, const int dump_ind, const int backup);
+
+/*@
+ @ requires \valid(disk);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk, partition);
+ @*/
int check_FAT(disk_t *disk, partition_t *partition, const int verbose);
+
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(fat_header);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk, partition, fat_header);
+ @*/
int test_FAT(disk_t *disk, const struct fat_boot_sector *fat_header, const partition_t *partition, const int verbose, const int dump_ind);
+
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(fat_header);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk, partition, fat_header);
+ @*/
int recover_OS2MB(const disk_t *disk, const struct fat_boot_sector*fat_header, partition_t *partition, const int verbose, const int dump_ind);
+
+/*@
+ @ requires \valid(disk);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk, partition);
+ @*/
int check_OS2MB(disk_t *disk, partition_t *partition, const int verbose);
+
+/*@
+ @ requires \valid_read(name);
+ @*/
int check_VFAT_volume_name(const char *name, const unsigned int max_size);
#ifdef __cplusplus
} /* closing brace for extern "C" */
diff --git a/src/file_dir.c b/src/file_dir.c
index 09a5b96..a91bdaa 100644
--- a/src/file_dir.c
+++ b/src/file_dir.c
@@ -50,6 +50,11 @@ const file_hint_t file_hint_dir= {
.register_header_check=&register_header_check_dir
};
+/*@
+ @ requires \valid(file_recovery);
+ @ requires valid_read_string((char*)&file_recovery->filename);
+ @ requires file_recovery->file_rename==&file_rename_fatdir;
+ @*/
static void file_rename_fatdir(file_recovery_t *file_recovery)
{
unsigned char buffer[512];
@@ -68,6 +73,15 @@ static void file_rename_fatdir(file_recovery_t *file_recovery)
file_rename(file_recovery, buffer_cluster, strlen(buffer_cluster), 0, NULL, 1);
}
+/*@
+ @ requires buffer_size >= 2;
+ @ requires (buffer_size&1)==0;
+ @ requires \valid_read((char *)buffer+(0..buffer_size-1));
+ @ requires \valid(file_recovery);
+ @ requires file_recovery->data_check == &data_check_fatdir;
+ @ ensures \result == DC_STOP;
+ @ assigns file_recovery->calculated_file_size;
+ @*/
static data_check_t data_check_fatdir(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
/* Save only one cluster */
@@ -75,6 +89,15 @@ static data_check_t data_check_fatdir(const unsigned char *buffer, const unsigne
return DC_STOP;
}
+/*@
+ @ requires buffer_size >= sizeof(struct msdos_dir_entry);
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ requires separation: \separated(&file_hint_dir, buffer+(..), file_recovery, file_recovery_new);
+ @*/
static int header_check_dir(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
{
const struct msdos_dir_entry *de=(const struct msdos_dir_entry*)buffer;
@@ -89,6 +112,9 @@ static int header_check_dir(const unsigned char *buffer, const unsigned int buff
return 1;
}
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_dir(file_stat_t *file_stat)
{
register_header_check(0, ". ", 8+3, &header_check_dir, file_stat);
diff --git a/src/file_tar.c b/src/file_tar.c
index 424b314..c777a6e 100644
--- a/src/file_tar.c
+++ b/src/file_tar.c
@@ -64,6 +64,15 @@ struct posix_header
/* 500 */
};
+/*@
+ @ requires buffer_size >= 512;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ requires separation: \separated(&file_hint_tar, buffer+(..), file_recovery, file_recovery_new);
+ @*/
int header_check_tar(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
{
const struct posix_header *h=(const struct posix_header *)buffer;
@@ -80,6 +89,9 @@ int header_check_tar(const unsigned char *buffer, const unsigned int buffer_size
return 1;
}
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_tar(file_stat_t *file_stat)
{
static const unsigned char tar_header_gnu[6] = { 'u','s','t','a','r',0x00};
diff --git a/src/fnctdsk.c b/src/fnctdsk.c
index 0a766b2..f483ce2 100644
--- a/src/fnctdsk.c
+++ b/src/fnctdsk.c
@@ -38,8 +38,17 @@
#include "log_part.h"
#include "guid_cpy.h"
-static unsigned int get_geometry_from_list_part_aux(const disk_t *disk_car, const list_part_t *list_part, const int verbose);
-static list_part_t *element_new(partition_t *part);
+/*@
+ @ requires \valid(part);
+ @*/
+static list_part_t *element_new(partition_t *part)
+{
+ list_part_t *new_element=(list_part_t*)MALLOC(sizeof(*new_element));
+ new_element->part=part;
+ new_element->prev=new_element->next=NULL;
+ new_element->to_be_removed=0;
+ return new_element;
+}
unsigned long int C_H_S2LBA(const disk_t *disk_car,const unsigned int C, const unsigned int H, const unsigned int S)
{
@@ -318,19 +327,16 @@ partition_t *partition_new(const arch_fnct_t *arch)
return partition;
}
-static list_part_t *element_new(partition_t *part)
-{
- list_part_t *new_element=(list_part_t*)MALLOC(sizeof(*new_element));
- new_element->part=part;
- new_element->prev=new_element->next=NULL;
- new_element->to_be_removed=0;
- return new_element;
-}
-
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(list_part);
+ @ assigns \nothing;
+ @*/
static unsigned int get_geometry_from_list_part_aux(const disk_t *disk_car, const list_part_t *list_part, const int verbose)
{
const list_part_t *element;
unsigned int nbr=0;
+ /*@ loop assigns element, nbr; */
for(element=list_part;element!=NULL;element=element->next)
{
CHS_t start;
diff --git a/src/fnctdsk.h b/src/fnctdsk.h
index e979309..1c8a611 100644
--- a/src/fnctdsk.h
+++ b/src/fnctdsk.h
@@ -23,29 +23,190 @@
extern "C" {
#endif
+/*@
+ @ requires \valid_read(disk_car);
+ @ assigns \nothing;
+ @*/
unsigned long int C_H_S2LBA(const disk_t *disk_car,const unsigned int C, const unsigned int H, const unsigned int S);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ assigns \nothing;
+ @*/
uint64_t CHS2offset(const disk_t *disk_car,const CHS_t*CHS);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires disk_car->sector_size > 0;
+ @ requires disk_car->geom.sectors_per_head > 0;
+ @ assigns \nothing;
+ @ ensures 0 < \result <= disk_car->geom.sectors_per_head;
+ @*/
unsigned int offset2sector(const disk_t *disk_car, const uint64_t offset);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires disk_car->sector_size > 0;
+ @ requires disk_car->geom.sectors_per_head > 0;
+ @ requires disk_car->geom.heads_per_cylinder > 0;
+ @ assigns \nothing;
+ @ ensures \result <= disk_car->geom.heads_per_cylinder;
+ @*/
unsigned int offset2head(const disk_t *disk_car, const uint64_t offset);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires disk_car->sector_size > 0;
+ @ requires disk_car->geom.sectors_per_head > 0;
+ @ requires disk_car->geom.heads_per_cylinder > 0;
+ @ assigns \nothing;
+ @*/
unsigned int offset2cylinder(const disk_t *disk_car, const uint64_t offset);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid(CHS);
+ @ requires disk_car->sector_size > 0;
+ @ requires disk_car->geom.sectors_per_head > 0;
+ @ requires disk_car->geom.heads_per_cylinder > 0;
+ @ assigns CHS->cylinder,CHS->head,CHS->sector;
+ @*/
void offset2CHS(const disk_t *disk_car,const uint64_t offset, CHS_t*CHS);
+/*@
+ @ requires list_disk==\null || \valid(list_disk);
+ @ requires disk==\null || (\valid(disk) && valid_read_string(disk->device));
+ @ requires the_disk==\null || \valid(the_disk);
+ @ ensures \result==\null || \valid(\result);
+ @ ensures disk==\null ==> \result == list_disk;
+ @*/
list_disk_t *insert_new_disk_aux(list_disk_t *list_disk, disk_t *disk, disk_t **the_disk);
+
+/*@
+ @ requires list_disk==\null || \valid(list_disk);
+ @ requires disk_car==\null || (\valid(disk_car) && valid_read_string(disk_car->device));
+ @ ensures \result==\null || \valid(\result);
+ @*/
list_disk_t *insert_new_disk(list_disk_t *list_disk, disk_t *disk_car);
+
+/*@
+ @ requires list_part == \null || \valid(list_part);
+ @ requires \valid(part);
+ @ requires \valid(insert_error);
+ @*/
list_part_t *insert_new_partition(list_part_t *list_part, partition_t *part, const int force_insert, int *insert_error);
+
+/*@
+ @ requires \valid(list_part);
+ @*/
list_part_t *sort_partition_list(list_part_t *list_part);
+
+/*@
+ @ requires \valid_read(list_part);
+ @*/
list_part_t *gen_sorted_partition_list(const list_part_t *list_part);
+
+/*@
+ @ requires \valid(list_part);
+ @*/
void part_free_list(list_part_t *list_part);
+
+/*@
+ @ requires \valid(list_part);
+ @*/
void part_free_list_only(list_part_t *list_part);
+
+/*@
+ @ requires \valid(partition);
+ @ requires \valid_read(arch);
+ @ assigns partition->part_size;
+ @ assigns partition->sborg_offset;
+ @ assigns partition->sb_offset;
+ @ assigns partition->sb_size;
+ @ assigns partition->blocksize;
+ @ assigns partition->part_type_i386;
+ @ assigns partition->part_type_sun;
+ @ assigns partition->part_type_mac;
+ @ assigns partition->part_type_xbox;
+ @ assigns partition->part_type_gpt;
+ @ assigns partition->part_uuid;
+ @ assigns partition->upart_type;
+ @ assigns partition->status;
+ @ assigns partition->order;
+ @ assigns partition->errcode;
+ @ assigns partition->fsname[0];
+ @ assigns partition->partname[0];
+ @ assigns partition->info[0];
+ @ ensures partition->part_size == 0;
+ @ ensures partition->sborg_offset == 0;
+ @ ensures partition->sb_offset == 0;
+ @ ensures partition->sb_size == 0;
+ @ ensures partition->blocksize == 0;
+ @ ensures partition->part_type_i386 == P_NO_OS;
+ @ ensures partition->part_type_sun == PSUN_UNK;
+ @ ensures partition->part_type_mac == PMAC_UNK;
+ @ ensures partition->part_type_xbox == PXBOX_UNK;
+ @ ensures partition->upart_type == UP_UNK;
+ @ ensures partition->status == STATUS_DELETED;
+ @ ensures partition->order == NO_ORDER;
+ @ ensures partition->errcode == BAD_NOERR;
+ @ ensures partition->fsname[0] == '\0';
+ @ ensures partition->partname[0] == '\0';
+ @ ensures partition->info[0] == '\0';
+ @ ensures partition->arch == arch;
+ @*/
void partition_reset(partition_t *partition, const arch_fnct_t *arch);
+
+/*@
+ @ requires \valid_read(arch);
+ @ ensures \result->arch == arch;
+ @*/
partition_t *partition_new(const arch_fnct_t *arch);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(list_part);
+ @ assigns \nothing;
+ @*/
unsigned int get_geometry_from_list_part(const disk_t *disk_car, const list_part_t *list_part, const int verbose);
+
+/*@
+ @ requires list_disk==\null || \valid(list_disk);
+ @ requires list_disk==\null || \freeable(list_disk);
+ @ requires list_disk==\null || \freeable(list_disk->disk);
+ @ requires list_disk==\null || (list_disk->disk->device == \null || \freeable(list_disk->disk->device));
+ @ requires list_disk==\null || (list_disk->disk->model == \null || \freeable(list_disk->disk->model));
+ @ requires list_disk==\null || (list_disk->disk->serial_no == \null || \freeable(list_disk->disk->serial_no));
+ @ requires list_disk==\null || (list_disk->disk->fw_rev == \null || \freeable(list_disk->disk->fw_rev));
+ @ requires list_disk==\null || (list_disk->disk->data == \null || \freeable(list_disk->disk->data));
+ @ requires list_disk==\null || (list_disk->disk->rbuffer == \null || \freeable(list_disk->disk->rbuffer));
+ @ requires list_disk==\null || (list_disk->disk->wbuffer == \null || \freeable(list_disk->disk->wbuffer));
+ @*/
int delete_list_disk(list_disk_t *list_disk);
+
+/*@
+ @ requires \valid(buffer + (0..99));
+ @ ensures valid_string(buffer);
+ @*/
+/* TODO assigns */
void size_to_unit(const uint64_t disk_size, char *buffer);
+
+/*@
+ @ requires \valid_read(list_part);
+ @ assigns \nothing;
+ @*/
int is_part_overlapping(const list_part_t *list_part);
+
+/*@
+ @ requires \valid(dest);
+ @ requires \valid_read(src);
+ @*/
void dup_partition_t(partition_t *dest, const partition_t *src);
-void log_disk_list(list_disk_t *list_disk);
+/*@
+ @ requires list_disk==\null || \valid(list_disk);
+ @*/
+void log_disk_list(list_disk_t *list_disk);
#ifdef __cplusplus
} /* closing brace for extern "C" */
#endif
diff --git a/src/geometry.c b/src/geometry.c
index 470ab60..98f4d75 100644
--- a/src/geometry.c
+++ b/src/geometry.c
@@ -80,6 +80,7 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
if(*current_cmd==NULL)
return 0;
log_info("Current geometry\n%s sector_size=%u\n", disk_car->description(disk_car), disk_car->sector_size);
+ /*@ loop invariant valid_read_string(*current_cmd); */
while (done==0)
{
skip_comma_in_command(current_cmd);
diff --git a/src/geometry.h b/src/geometry.h
index 98993c2..5534241 100644
--- a/src/geometry.h
+++ b/src/geometry.h
@@ -23,8 +23,29 @@
extern "C" {
#endif
+/*@
+ @ requires \valid(disk);
+ @ requires 0 < disk->geom.sectors_per_head;
+ @ requires 0 < disk->geom.heads_per_cylinder;
+ @ assigns disk->geom.cylinders;
+ @*/
void set_cylinders_from_size_up(disk_t *disk);
+
+/*@
+ @ requires \valid(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_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);
+ @*/
int change_geometry_cli(disk_t *disk, char **current_cmd);
#ifdef __cplusplus
diff --git a/src/guid_cmp.h b/src/guid_cmp.h
index 14ccde8..4c0aece 100644
--- a/src/guid_cmp.h
+++ b/src/guid_cmp.h
@@ -19,6 +19,10 @@
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
+
+/*@
+ @ assigns \nothing;
+ @*/
static inline int guid_cmp (const efi_guid_t left, const efi_guid_t right)
{
return memcmp(&left, &right, sizeof(efi_guid_t));
diff --git a/src/guid_cpy.h b/src/guid_cpy.h
index 5244a70..c68a087 100644
--- a/src/guid_cpy.h
+++ b/src/guid_cpy.h
@@ -19,6 +19,15 @@
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
+
+/*@ requires \valid(dst);
+ @ requires \valid_read(src);
+ @ requires separation:
+ @ \separated(((char *)dst)+(0..sizeof(efi_guid_t)-1),((char *)src)+(0..sizeof(efi_guid_t)-1));
+ @ assigns ((char*)dst)[0..sizeof(efi_guid_t) - 1];
+ @*/
+// assigns ((char*)dst)[0..sizeof(efi_guid_t) - 1] \from ((char*)src)[0..sizeof(efi_guid_t)-1];
+// ensures copied_contents: memcmp{Post,Pre}((char*)dst,(char*)src,sizeof(efi_guid_t)) == 0;
static inline void guid_cpy (efi_guid_t *dst, const efi_guid_t *src)
{
memcpy(dst, src, sizeof(efi_guid_t));
diff --git a/src/hdaccess.h b/src/hdaccess.h
index 01ffbcc..0aa7f0d 100644
--- a/src/hdaccess.h
+++ b/src/hdaccess.h
@@ -22,14 +22,88 @@
#ifdef __cplusplus
extern "C" {
#endif
-
-
+/*@
+ @ requires \valid(disk_car);
+ @ requires disk_car->sector_size > 0;
+ @ requires disk_car->geom.heads_per_cylinder > 0;
+ @ requires \valid_function(disk_car->pread);
+ @*/
void hd_update_geometry(disk_t *disk_car, const int verbose);
+
+/*@
+ @ requires list_disk==\null || \valid_read(list_disk);
+ @*/
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);
+ @*/
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));
+ @*/
disk_t *file_test_availability(const char *device, const int verbose, const int testdisk_mode);
+
+/*@
+ @ requires \valid(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;
+ @*/
void update_disk_car_fields(disk_t *disk_car);
+
+/*@
+ @ requires \valid(disk);
+ @ ensures disk->autodetect == 0;
+ @ ensures disk->disk_size == 0;
+ @ ensures disk->user_max == 0;
+ @ ensures disk->native_max == 0;
+ @ ensures disk->dco == 0;
+ @ ensures disk->offset == 0;
+ @ ensures disk->rbuffer == NULL;
+ @ ensures disk->wbuffer == NULL;
+ @ ensures disk->rbuffer_size == 0;
+ @ ensures disk->wbuffer_size == 0;
+ @ ensures disk->model == NULL;
+ @ ensures disk->serial_no == NULL;
+ @ ensures disk->fw_rev == NULL;
+ @ ensures disk->write_used == 0;
+ @ ensures disk->description_txt[0] == '\0';
+ @ ensures disk->unit == UNIT_CHS;
+ @ assigns disk->autodetect, disk->disk_size, disk->user_max, disk->native_max, disk->dco, disk->offset;
+ @ assigns disk->rbuffer, disk->wbuffer, disk->rbuffer_size, disk->wbuffer_size;
+ @ assigns disk->model, disk->serial_no, disk->fw_rev, disk->write_used;
+ @ assigns disk->description_txt[0], disk->unit;
+ @*/
void init_disk(disk_t *disk);
+
+/*@
+ @ requires \valid(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);
+ @*/
void generic_clean(disk_t *disk);
#ifdef __cplusplus
diff --git a/src/hdcache.h b/src/hdcache.h
index 4bc76dc..c32ad3a 100644
--- a/src/hdcache.h
+++ b/src/hdcache.h
@@ -23,6 +23,10 @@
extern "C" {
#endif
+/*@
+ @ requires \valid(disk_car);
+ @ ensures \valid(\result);
+ @*/
disk_t *new_diskcache(disk_t *disk_car, const unsigned int cache_size_min);
#ifdef __cplusplus
diff --git a/src/intrf.c b/src/intrf.c
index 3905015..ef2fa1b 100644
--- a/src/intrf.c
+++ b/src/intrf.c
@@ -201,6 +201,7 @@ const char *aff_part_aux(const unsigned int newline, const disk_t *disk_car, con
uint64_t atouint64(const char *nptr)
{
uint64_t tmp=0;
+ /*@ loop assigns tmp, nptr; */
while(*nptr >='0' && *nptr <= '9')
{
tmp = tmp * 10 + *nptr - '0';
@@ -215,7 +216,9 @@ uint64_t ask_number_cli(char **current_cmd, const uint64_t val_cur, const uint64
{
uint64_t tmp_val;
skip_comma_in_command(current_cmd);
+ /*@ assert valid_read_string(*current_cmd); */
tmp_val = get_int_from_command(current_cmd);
+ /*@ assert valid_read_string(*current_cmd); */
if (val_min==val_max || (tmp_val >= val_min && tmp_val <= val_max))
return tmp_val;
else
@@ -231,6 +234,7 @@ uint64_t ask_number_cli(char **current_cmd, const uint64_t val_cur, const uint64
va_end(ap);
}
}
+ /*@ assert valid_read_string(*current_cmd); */
return val_cur;
}
diff --git a/src/intrf.h b/src/intrf.h
index a50acfb..e675679 100644
--- a/src/intrf.h
+++ b/src/intrf.h
@@ -58,9 +58,18 @@ struct MenuItem
void log_CHS_from_LBA(const disk_t *disk_car, const unsigned long int pos_LBA);
const char *aff_part_aux(const unsigned int newline, const disk_t *disk_car, const partition_t *partition);
-void aff_part_buffer(const unsigned int newline,const disk_t *disk_car,const partition_t *partition);
+void aff_part_buffer(const unsigned int newline, const disk_t *disk_car, const partition_t *partition);
+/*@
+ @ requires valid_read_string(nptr);
+ @ assigns \nothing;
+ @*/
uint64_t atouint64(const char *nptr);
+
+/*@
+ @ requires valid_read_string(*current_cmd);
+ @ ensures valid_read_string(*current_cmd);
+ @*/
uint64_t ask_number_cli(char **current_cmd, const uint64_t val_cur, const uint64_t val_min, const uint64_t val_max, const char * _format, ...) __attribute__ ((format (printf, 5, 6)));
void screen_buffer_reset(void);
int screen_buffer_add(const char *_format, ...) __attribute__ ((format (printf, 1, 2)));
diff --git a/src/iso.h b/src/iso.h
index 3567a92..674352b 100644
--- a/src/iso.h
+++ b/src/iso.h
@@ -22,7 +22,18 @@
#ifdef __cplusplus
extern "C" {
#endif
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
int check_ISO(disk_t *disk_car, partition_t *partition);
+
+/*@
+ @ requires \valid_read(iso);
+ @ requires \valid(partition);
+ @ requires separation: \separated(iso, partition);
+ @*/
int recover_ISO(const struct iso_primary_descriptor *iso, partition_t *partition);
#ifdef __cplusplus
} /* closing brace for extern "C" */
diff --git a/src/jfs.h b/src/jfs.h
index 12b53dd..1ab5589 100644
--- a/src/jfs.h
+++ b/src/jfs.h
@@ -26,8 +26,20 @@ extern "C" {
#define JFS_SUPERBLOCK_SIZE 512
#define L2BPERDMAP 13 /* l2 num of blks per dmap */
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
int check_JFS(disk_t *disk_car, partition_t *partition);
-int recover_JFS(const disk_t *disk_car, const struct jfs_superblock *sb,partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(sb);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, sb, partition);
+ @*/
+int recover_JFS(const disk_t *disk_car, const struct jfs_superblock *sb, partition_t *partition, const int verbose, const int dump_ind);
#ifdef __cplusplus
} /* closing brace for extern "C" */
diff --git a/src/lvm.h b/src/lvm.h
index 2ca728d..404925a 100644
--- a/src/lvm.h
+++ b/src/lvm.h
@@ -90,8 +90,18 @@ typedef struct {
} pv_disk_v2_t;
#define pv_disk_t pv_disk_v2_t
-int check_LVM(disk_t *disk_car,partition_t *partition,const int verbose);
-int recover_LVM(const disk_t *disk_car, const pv_disk_t *pv,partition_t *partition,const int verbose, const int dump_ind);
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @*/
+int check_LVM(disk_t *disk_car, partition_t *partition, const int verbose);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(pv);
+ @ requires \valid(partition);
+ @*/
+int recover_LVM(const disk_t *disk_car, const pv_disk_t *pv, partition_t *partition, const int verbose, const int dump_ind);
#define LVM2_LABEL "LVM2 001"
#define LABEL_ID "LABELONE"
@@ -118,8 +128,20 @@ struct lvm2_pv_header {
struct lvm2_disk_locn disk_areas_xl[0]; /* Two lists */
} __attribute__ ((packed));
-int check_LVM2(disk_t *disk_car,partition_t *partition,const int verbose);
-int recover_LVM2(const disk_t *disk_car, const unsigned char *buf,partition_t *partition,const int verbose, const int dump_ind);
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
+int check_LVM2(disk_t *disk_car, partition_t *partition, const int verbose);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(buf);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, buf, partition);
+ @*/
+int recover_LVM2(const disk_t *disk_car, const unsigned char *buf, partition_t *partition, const int verbose, const int dump_ind);
#ifdef __cplusplus
} /* closing brace for extern "C" */
diff --git a/src/md.h b/src/md.h
index 6cedc58..e810fb0 100644
--- a/src/md.h
+++ b/src/md.h
@@ -253,8 +253,26 @@ static inline uint64_t md_event(mdp_super_t *sb) {
#endif
/* TestDisk */
-int check_MD(disk_t *disk_car,partition_t *partition,const int verbose);
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
+int check_MD(disk_t *disk_car, partition_t *partition, const int verbose);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(sb);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, sb, partition);
+ @*/
int recover_MD(const disk_t *disk_car, const struct mdp_superblock_s *sb, partition_t *partition, const int verbose, const int dump_ind);
+
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
int recover_MD_from_partition(disk_t *disk_car, partition_t *partition, const int verbose);
#ifdef __cplusplus
diff --git a/src/misc.h b/src/misc.h
index 28b0c60..e2f23ea 100644
--- a/src/misc.h
+++ b/src/misc.h
@@ -23,9 +23,14 @@
extern "C" {
#endif
+/*@ ensures valid_read_string(\result); */
const char *get_os(void);
+
+/*@ ensures valid_read_string(\result); */
const char *get_compiler(void);
+
#ifdef RECORD_COMPILATION_DATE
+/*@ ensures valid_read_string(\result); */
const char *get_compilation_date(void);
#endif
diff --git a/src/netware.h b/src/netware.h
index d2c8dcc..2416562 100644
--- a/src/netware.h
+++ b/src/netware.h
@@ -32,7 +32,19 @@ struct disk_netware
int32_t nbr_sectors;
};
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
int check_netware(disk_t *disk_car, partition_t *partition);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(netware_block);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, netware_block, partition);
+ @*/
int recover_netware(const disk_t *disk_car, const struct disk_netware *netware_block, partition_t *partition);
#ifdef __cplusplus
diff --git a/src/ntfs_utl.c b/src/ntfs_utl.c
index e18848c..438ae50 100644
--- a/src/ntfs_utl.c
+++ b/src/ntfs_utl.c
@@ -26,6 +26,12 @@
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
+
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_LIBNTFS
+#undef HAVE_LIBNTFS3G
+#endif
+
#if defined(HAVE_LIBNTFS) || defined(HAVE_LIBNTFS3G)
#include <stdio.h>
#ifdef HAVE_STDLIB_H
diff --git a/src/partauto.h b/src/partauto.h
index a1a1a51..7d51838 100644
--- a/src/partauto.h
+++ b/src/partauto.h
@@ -23,6 +23,11 @@
extern "C" {
#endif
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(arch);
+ @ requires separation: \separated(disk, arch);
+ @*/
void autodetect_arch(disk_t *disk, const arch_fnct_t *arch);
#ifdef __cplusplus
diff --git a/src/partgpt.c b/src/partgpt.c
index 34ee5a6..add4e51 100644
--- a/src/partgpt.c
+++ b/src/partgpt.c
@@ -398,6 +398,7 @@ list_part_t *add_partition_gpt_cli(const disk_t *disk_car, list_part_t *list_par
new_partition=partition_new(&arch_gpt);
new_partition->part_offset=disk_car->sector_size;
new_partition->part_size=disk_car->disk_size-new_partition->part_offset;
+ /*@ loop invariant valid_read_string(*current_cmd); */
while(1)
{
skip_comma_in_command(current_cmd);
@@ -571,6 +572,7 @@ static int check_part_gpt(disk_t *disk, const int verbose,partition_t *partition
static const char *get_gpt_typename(const efi_guid_t part_type_gpt)
{
int i;
+ /*@ loop assigns i; */
for(i=0; gpt_sys_types[i].name!=NULL; i++)
if(guid_cmp(gpt_sys_types[i].part_type, part_type_gpt)==0)
return gpt_sys_types[i].name;
diff --git a/src/partgpt.h b/src/partgpt.h
index c3994c6..34c93ed 100644
--- a/src/partgpt.h
+++ b/src/partgpt.h
@@ -62,7 +62,20 @@ struct systypes_gtp {
const char *name;
};
-list_part_t *add_partition_gpt_cli(const disk_t *disk_car,list_part_t *list_part, char **current_cmd);
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid(list_part);
+ @ requires separation: \separated(disk_car, list_part, current_cmd);
+ @ requires \valid(current_cmd);
+ @ requires valid_string(*current_cmd);
+ @*/
+list_part_t *add_partition_gpt_cli(const disk_t *disk_car, list_part_t *list_part, char **current_cmd);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid(list_part);
+ @ requires separation: \separated(disk_car, list_part);
+ @*/
int write_part_gpt(disk_t *disk_car, const list_part_t *list_part, const int ro, const int verbose);
#ifdef __cplusplus
diff --git a/src/parthumax.c b/src/parthumax.c
index d1b5e47..4858e6d 100644
--- a/src/parthumax.c
+++ b/src/parthumax.c
@@ -241,6 +241,7 @@ 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); */
while(1)
{
skip_comma_in_command(current_cmd);
diff --git a/src/parti386.c b/src/parti386.c
index 0b010b9..6e2160b 100644
--- a/src/parti386.c
+++ b/src/parti386.c
@@ -384,6 +384,10 @@ static unsigned int get_part_type_i386(const partition_t *partition)
return partition->part_type_i386;
}
+/*@
+ @ requires \valid(cp);
+ @ assigns cp[0 .. 3];
+ @*/
static void store4_little_endian(unsigned char *cp, unsigned int val)
{
cp[0] = (val & 0xff);
@@ -392,43 +396,65 @@ static void store4_little_endian(unsigned char *cp, unsigned int val)
cp[3] = ((val >> 24) & 0xff);
}
+/*@
+ @ requires \valid_read(cp);
+ @ assigns \nothing;
+ @*/
static unsigned int read4_little_endian(const unsigned char *cp)
{
return (unsigned int)(cp[0]) + ((unsigned int)(cp[1]) << 8) + ((unsigned int)(cp[2]) << 16) + ((unsigned int)(cp[3]) << 24);
}
+/*@
+ @ requires \valid_read(p);
+ @ assigns \nothing;
+ @*/
static uint64_t get_start_sect(const struct partition_dos *p)
{
return read4_little_endian(p->start4);
}
+/*@
+ @ requires \valid_read(p);
+ @ assigns \nothing;
+ @*/
static uint64_t get_nr_sects(const struct partition_dos *p)
{
return read4_little_endian(p->size4);
}
+/*@
+ @ requires \valid(p);
+ @ assigns p->size4[0 .. 3];
+ @*/
static void set_nr_sects(struct partition_dos *p, unsigned int nr_sects)
{
store4_little_endian(p->size4, nr_sects);
}
+/*@
+ @ requires \valid(p);
+ @ assigns p->start4[0 .. 3];
+ @*/
static void set_start_sect(struct partition_dos *p, unsigned int start_sect)
{
store4_little_endian(p->start4, start_sect);
}
-
static int get_geometry_from_i386mbr(const unsigned char *buffer, const int verbose, CHSgeometry_t *geometry)
{
unsigned int i;
+#ifndef __FRAMAC__
if(verbose>1)
{
log_trace("get_geometry_from_i386mbr\n");
}
+#endif
if((buffer[0x1FE]!=(unsigned char)0x55)||(buffer[0x1FF]!=(unsigned char)0xAA))
{
return 1;
}
+ /*@ loop assigns i, geometry->cylinders, geometry->heads_per_cylinder, geometry->sectors_per_head; */
for(i=0;i<4;i++)
{
const struct partition_dos *p=pt_offset_const(buffer,i);
@@ -1373,6 +1399,7 @@ 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); */
while(1)
{
skip_comma_in_command(current_cmd);
@@ -1783,6 +1810,7 @@ static int check_part_i386(disk_t *disk_car,const int verbose,partition_t *parti
static const char *get_partition_typename_i386_aux(const unsigned int part_type_i386)
{
int i;
+ /*@ loop assigns i; */
for (i=0; i386_sys_types[i].name!=NULL; i++)
if (i386_sys_types[i].part_type == part_type_i386)
return i386_sys_types[i].name;
diff --git a/src/parti386.h b/src/parti386.h
index fde6957..c1f5e2a 100644
--- a/src/parti386.h
+++ b/src/parti386.h
@@ -23,8 +23,29 @@
extern "C" {
#endif
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
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(current_cmd);
+ @ requires valid_read_string(*current_cmd);
+ @ requires separation: \separated(disk_car, list_part, current_cmd);
+ @ 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);
+
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(buffer + (0 .. 512-1));
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk, buffer + (0 .. 512-1), partition);
+ @*/
int recover_i386_logical(disk_t *disk, const unsigned char *buffer, partition_t *partition);
#ifdef __cplusplus
diff --git a/src/partmac.c b/src/partmac.c
index cbcb1b7..a9f1cba 100644
--- a/src/partmac.c
+++ b/src/partmac.c
@@ -48,16 +48,72 @@
#include "hfsp.h"
#include "log.h"
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @*/
static int check_part_mac(disk_t *disk_car, const int verbose,partition_t *partition,const int saveheader);
+
+/*@
+ @ requires \valid(disk_car);
+ @*/
static list_part_t *read_part_mac(disk_t *disk_car, const int verbose, const int saveheader);
+
+/*@
+ @ requires \valid(disk_car);
+ @ requires list_part == \null || \valid(list_part);
+ @*/
static int write_part_mac(disk_t *disk_car, const list_part_t *list_part, const int ro , const int verbose);
+
+/*@
+ @ requires \valid(disk_car);
+ @ requires list_part == \null || \valid(list_part);
+ @ requires separation: \separated(disk_car, list_part);
+ @ assigns \nothing;
+ @*/
static list_part_t *init_part_order_mac(const disk_t *disk_car, list_part_t *list_part);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @ assigns partition->status;
+ @*/
static void set_next_status_mac(const disk_t *disk_car, partition_t *partition);
+
+/*@
+ @ requires \valid(partition);
+ @ assigns partition->part_type_mac;
+ @*/
static int set_part_type_mac(partition_t *partition, unsigned int part_type_mac);
+
+/*@
+ @ requires \valid(partition);
+ @ assigns \nothing;
+ @*/
static int is_part_known_mac(const partition_t *partition);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires list_part == \null || \valid(list_part);
+ @*/
static void init_structure_mac(const disk_t *disk_car,list_part_t *list_part, const int verbose);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
static const char *get_partition_typename_mac(const partition_t *partition);
+
+/*@
+ @ assigns \nothing;
+ @*/
static const char *get_partition_typename_mac_aux(const unsigned int part_type_mac);
+
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
static unsigned int get_part_type_mac(const partition_t *partition);
static const struct systypes mac_sys_types[] = {
@@ -396,6 +452,7 @@ static int check_part_mac(disk_t *disk_car,const int verbose,partition_t *partit
static const char *get_partition_typename_mac_aux(const unsigned int part_type_mac)
{
int i;
+ /*@ loop assigns i; */
for (i=0; mac_sys_types[i].name!=NULL; i++)
if (mac_sys_types[i].part_type == part_type_mac)
return mac_sys_types[i].name;
diff --git a/src/partnone.c b/src/partnone.c
index 7122104..f354941 100644
--- a/src/partnone.c
+++ b/src/partnone.c
@@ -528,15 +528,23 @@ static int check_part_none(disk_t *disk_car,const int verbose,partition_t *parti
return ret;
}
+/*@
+ @ assigns \nothing;
+ @*/
static const char *get_partition_typename_none_aux(const unsigned int part_type_none)
{
int i;
+ /*@ loop assigns i; */
for (i=0; none_sys_types[i].name!=NULL; i++)
if (none_sys_types[i].part_type == part_type_none)
return none_sys_types[i].name;
return NULL;
}
+/*@
+ @ requires \valid_read(partition);
+ @ assigns \nothing;
+ @*/
static const char *get_partition_typename_none(const partition_t *partition)
{
return get_partition_typename_none_aux(partition->upart_type);
diff --git a/src/partsun.c b/src/partsun.c
index 4698ff9..93e1400 100644
--- a/src/partsun.c
+++ b/src/partsun.c
@@ -175,18 +175,22 @@ static unsigned int get_part_type_sun(const partition_t *partition)
static int get_geometry_from_sunmbr(const unsigned char *buffer, const int verbose, CHSgeometry_t *geometry)
{
const sun_disklabel *sunlabel=(const sun_disklabel*)buffer;
+#ifndef __FRAMAC__
if(verbose>1)
{
log_trace("get_geometry_from_sunmbr\n");
}
+#endif
geometry->cylinders=0;
geometry->heads_per_cylinder=be16(sunlabel->ntrks);
geometry->sectors_per_head=be16(sunlabel->nsect);
+#ifndef __FRAMAC__
if(geometry->sectors_per_head>0)
{
log_info("Geometry from SUN MBR: head=%u sector=%u\n",
geometry->heads_per_cylinder, geometry->sectors_per_head);
}
+#endif
return 0;
}
@@ -290,6 +294,7 @@ 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); */
while(1)
{
skip_comma_in_command(current_cmd);
@@ -446,6 +451,7 @@ static int check_part_sun(disk_t *disk_car,const int verbose,partition_t *partit
static const char *get_partition_typename_sun_aux(const unsigned int part_type_sun)
{
int i;
+ /*@ loop assigns i; */
for (i=0; sun_sys_types[i].name!=NULL; i++)
if (sun_sys_types[i].part_type == part_type_sun)
return sun_sys_types[i].name;
diff --git a/src/partxbox.c b/src/partxbox.c
index fd04e9a..a9704b4 100644
--- a/src/partxbox.c
+++ b/src/partxbox.c
@@ -212,6 +212,7 @@ 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); */
while(1)
{
skip_comma_in_command(current_cmd);
@@ -364,6 +365,7 @@ static int check_part_xbox(disk_t *disk_car,const int verbose,partition_t *parti
static const char *get_partition_typename_xbox_aux(const unsigned int part_type_xbox)
{
int i;
+ /*@ loop assigns i; */
for (i=0; xbox_sys_types[i].name!=NULL; i++)
if (xbox_sys_types[i].part_type == part_type_xbox)
return xbox_sys_types[i].name;
diff --git a/src/pdiskseln.h b/src/pdiskseln.h
index 99f6c7d..2fb122c 100644
--- a/src/pdiskseln.h
+++ b/src/pdiskseln.h
@@ -23,6 +23,14 @@
extern "C" {
#endif
+/*@
+ @ requires \valid(params);
+ @ requires \valid(options);
+ @ requires list_disk == \null || \valid_read(list_disk);
+ @ requires params->cmd_device==\null || valid_read_string(params->cmd_device);
+ @ requires params->cmd_run==\null || valid_read_string(params->cmd_run);
+ @ ensures params->cmd_run==\null || valid_read_string(params->cmd_run);
+ @*/
int do_curses_photorec(struct ph_param *params, struct ph_options *options, const list_disk_t *list_disk);
#ifdef __cplusplus
diff --git a/src/phcli.c b/src/phcli.c
index 952d13d..f05a89e 100644
--- a/src/phcli.c
+++ b/src/phcli.c
@@ -44,6 +44,11 @@
extern int need_to_stop;
typedef enum { INIT_SPACE_WHOLE, INIT_SPACE_PREINIT, INIT_SPACE_EXT2_GROUP, INIT_SPACE_EXT2_INODE } init_mode_t;
+/*@
+ @ requires \valid_read(a);
+ @ requires \valid_read(b);
+ @ assigns \nothing;
+ @*/
static int spacerange_cmp(const struct td_list_head *a, const struct td_list_head *b)
{
const alloc_data_t *space_a=td_list_entry_const(a, const alloc_data_t, list);
diff --git a/src/phcli.h b/src/phcli.h
index 263ca47..78e1b52 100644
--- a/src/phcli.h
+++ b/src/phcli.h
@@ -23,6 +23,12 @@
extern "C" {
#endif
+/*@
+ @ requires \valid(list_part);
+ @ requires \valid(params);
+ @ requires \valid(options);
+ @ requires \valid(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 8af3bf7..08fa7c8 100644
--- a/src/phmain.c
+++ b/src/phmain.c
@@ -31,6 +31,7 @@
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#undef HAVE_DUP2
#undef HAVE_LIBEWF
+#undef HAVE_SIGACTION
#endif
#include <stdio.h>
diff --git a/src/photorec.h b/src/photorec.h
index 07bb345..7b3345d 100644
--- a/src/photorec.h
+++ b/src/photorec.h
@@ -68,13 +68,30 @@ int get_prev_file_header(const alloc_data_t *list_search_space, alloc_data_t **c
int file_finish_bf(file_recovery_t *file_recovery, struct ph_param *params,
alloc_data_t *list_search_space);
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(params);
+ @ requires \valid(list_search_space);
+ @ ensures \result == PFSTATUS_BAD || \result == PFSTATUS_OK || \result == PFSTATUS_OK_TRUNCATED;
+ @*/
pfstatus_t file_finish2(file_recovery_t *file_recovery, struct ph_param *params, const int paranoid, alloc_data_t *list_search_space);
+
void write_stats_log(const file_stat_t *file_stats);
void update_stats(file_stat_t *file_stats, alloc_data_t *list_search_space);
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);
void update_blocksize(const unsigned int blocksize, alloc_data_t *list_search_space, const uint64_t offset);
void forget(const alloc_data_t *list_search_space, alloc_data_t *current_search_space);
+
+/*@
+ @ requires \valid(list_search_space);
+ @ requires \valid_read(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);
unsigned int remove_used_space(disk_t *disk_car, const partition_t *partition, alloc_data_t *list_search_space);
void free_list_search_space(alloc_data_t *list_search_space);
@@ -87,6 +104,13 @@ uint64_t set_search_start(struct ph_param *params, alloc_data_t **new_current_se
void params_reset(struct ph_param *params, const struct ph_options *options);
const char *status_to_name(const photorec_status_t status);
void status_inc(struct ph_param *params, const struct ph_options *options);
+
+/*@
+ @ requires \valid(disk);
+ @ requires \valid_read(&disk->arch);
+ @ requires \valid_function(disk->arch->read_part);
+ @ requires \valid_read(options);
+ @*/
list_part_t *init_list_part(disk_t *disk, const struct ph_options *options);
void file_block_log(const file_recovery_t *file_recovery, const unsigned int sector_size);
void file_block_free(alloc_list_t *list_allocation);
diff --git a/src/poptions.c b/src/poptions.c
index 97cb3d9..116ba19 100644
--- a/src/poptions.c
+++ b/src/poptions.c
@@ -38,6 +38,7 @@ void interface_options_photorec_cli(struct ph_options *options, char **current_c
{
if(*current_cmd==NULL)
return ;
+ /*@ loop invariant valid_read_string(*current_cmd); */
while(1)
{
skip_comma_in_command(current_cmd);
diff --git a/src/poptions.h b/src/poptions.h
index 28abf6c..9ad1276 100644
--- a/src/poptions.h
+++ b/src/poptions.h
@@ -23,7 +23,17 @@
extern "C" {
#endif
+/*@
+ @ requires \valid(current_cmd);
+ @ requires valid_read_string(*current_cmd);
+ @ requires \valid(options);
+ @ ensures valid_read_string(*current_cmd);
+ @ */
void interface_options_photorec_cli(struct ph_options *options, char**current_cmd);
+
+/*@
+ @ requires \valid_read(options);
+ @ */
void interface_options_photorec_log(const struct ph_options *options);
#ifdef __cplusplus
diff --git a/src/rfs.h b/src/rfs.h
index 4cbedab..0642706 100644
--- a/src/rfs.h
+++ b/src/rfs.h
@@ -105,8 +105,20 @@ struct format40_super {
char sb_unused[432];
} __attribute__((packed));
-int check_rfs(disk_t *disk_car,partition_t *partition,const int verbose);
-int recover_rfs(const disk_t *disk_car, const struct reiserfs_super_block *sb,partition_t *partition,const int verbose, const int dump_ind);
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
+int check_rfs(disk_t *disk_car, partition_t *partition, const int verbose);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(sb);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, sb, partition);
+ @*/
+int recover_rfs(const disk_t *disk_car, const struct reiserfs_super_block *sb, partition_t *partition, const int verbose, const int dump_ind);
#ifdef __cplusplus
} /* closing brace for extern "C" */
diff --git a/src/sun.h b/src/sun.h
index b747b46..a59d9c4 100644
--- a/src/sun.h
+++ b/src/sun.h
@@ -77,8 +77,20 @@ typedef struct struct_sun_partition_i386 sun_partition_i386;
#define SUN_LABEL_MAGIC 0xDABE
#define SUN_LABEL_MAGIC_START 0x600DDEEE
-int recover_sun_i386(const disk_t *disk_car, const sun_partition_i386 *sunlabel, partition_t *partition,const int verbose, const int dump_ind);
-int check_sun_i386(disk_t *disk_car,partition_t *partition,const int verbose);
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid_read(sunlabel);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, sunlabel, partition);
+ @*/
+int recover_sun_i386(const disk_t *disk_car, const sun_partition_i386 *sunlabel, partition_t *partition, const int verbose, const int dump_ind);
+
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
+int check_sun_i386(disk_t *disk_car, partition_t *partition, const int verbose);
#ifdef __cplusplus
} /* closing brace for extern "C" */
diff --git a/src/swap.h b/src/swap.h
index 831b85d..cd1d1a0 100644
--- a/src/swap.h
+++ b/src/swap.h
@@ -49,7 +49,18 @@ union swap_header {
} magic8k;
};
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
int check_Linux_SWAP(disk_t *disk_car, partition_t *partition);
+
+/*@
+ @ requires \valid_read(swap_header);
+ @ requires \valid(partition);
+ @ requires separation: \separated(swap_header, partition);
+ @*/
int recover_Linux_SWAP(const union swap_header *swap_header, partition_t *partition);
#ifdef __cplusplus
diff --git a/src/ufs.h b/src/ufs.h
index 3b3bf47..88229e4 100644
--- a/src/ufs.h
+++ b/src/ufs.h
@@ -469,9 +469,20 @@ struct ufs_super_block {
#define UFS_42POSTBLFMT -1 /* 4.2BSD rotational table format */
#define UFS_DYNAMICPOSTBLFMT 1 /* dynamic rotational table format */
-
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
int check_ufs(disk_t *disk_car,partition_t *partition,const int verbose);
-int recover_ufs(const disk_t *disk_car, const struct ufs_super_block *sb, partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(sb);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, sb, partition);
+ @*/
+int recover_ufs(const disk_t *disk_car, const struct ufs_super_block *sb, partition_t *partition, const int verbose, const int dump_ind);
#ifdef __cplusplus
} /* closing brace for extern "C" */
diff --git a/src/xfs.h b/src/xfs.h
index 25838db..935da1c 100644
--- a/src/xfs.h
+++ b/src/xfs.h
@@ -107,7 +107,20 @@ struct xfs_sb
uint32_t sb_features2; /* additonal feature bits */
} __attribute__ ((gcc_struct, __packed__));
-int check_xfs(disk_t *disk_car,partition_t *partition,const int verbose);
+
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, partition);
+ @*/
+int check_xfs(disk_t *disk_car, partition_t *partition, const int verbose);
+
+/*@
+ @ requires \valid_read(disk_car);
+ @ requires \valid_read(sb);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk_car, sb, partition);
+ @*/
int recover_xfs(const disk_t *disk_car, const struct xfs_sb *sb, partition_t *partition, const int verbose, const int dump_ind);
#ifdef __cplusplus
diff --git a/src/zfs.h b/src/zfs.h
index b7f2b26..0e37630 100644
--- a/src/zfs.h
+++ b/src/zfs.h
@@ -37,8 +37,21 @@ struct vdev_boot_header {
uint64_t vb_size; /* size (bytes) */
char vb_pad[VDEV_BOOT_HEADER_SIZE - 4 * sizeof (uint64_t)];
};
-int check_ZFS(disk_t *disk,partition_t *partition);
-int recover_ZFS(const disk_t *disk, const struct vdev_boot_header *ZFS_header,partition_t *partition,const int verbose, const int dump_ind);
+
+/*@
+ @ requires \valid(disk);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk, partition);
+ @*/
+int check_ZFS(disk_t *disk, partition_t *partition);
+
+/*@
+ @ requires \valid_read(disk);
+ @ requires \valid_read(ZFS_header);
+ @ requires \valid(partition);
+ @ requires separation: \separated(disk, ZFS_header, partition);
+ @*/
+int recover_ZFS(const disk_t *disk, const struct vdev_boot_header *ZFS_header, partition_t *partition, const int verbose, const int dump_ind);
#ifdef __cplusplus
} /* closing brace for extern "C" */
#endif