luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Improve Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2022-07-14 10:09:09 +02:00
parent beaac3153e
commit 4e44db2b46
50 changed files with 138 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/alignio.h
View file

@ -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),

12
src/analyse.h
View file

@ -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);

1
src/apfs.h
View file

@ -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);

1
src/bfs.h
View file

@ -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);

1
src/bsd.h
View file

@ -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);

1
src/btrfs.h
View file

@ -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);

1
src/chgtype.h
View file

@ -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);

1
src/cramfs.h
View file

@ -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);

2
src/exfat.h
View file

@ -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);

1
src/exfatp.h
View file

@ -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);

1
src/ext2.h
View file

@ -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);

2
src/ext2grp.h
View file

@ -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);

1
src/f2fs.h
View file

@ -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);

6
src/fat.h
View file

@ -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);

1
src/fat_cluster.h
View file

@ -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);

1
src/fat_dir.h
View file

@ -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);

3
src/fatp.c
View file

@ -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)
{

1
src/fatp.h
View file

@ -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);

2
src/filegen.h
View file

@ -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);

1
src/gfs2.h
View file

@ -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);

6
src/hdaccess.h
View file

@ -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);

1
src/hfs.h
View file

@ -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);

2
src/hfsp.h
View file

@ -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);

1
src/hpfs.h
View file

@ -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);

2
src/io_redir.c
View file

@ -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);

1
src/iso.h
View file

@ -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);

1
src/jfs.h
View file

@ -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);

6
src/list_sort.c
View file

@ -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,

1
src/luks.h
View file

@ -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);

1
src/netware.h
View file

@ -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);

33
src/ntfs.c
View file

@ -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;
}

1
src/ntfs.h
View file

@ -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);

1
src/partauto.h
View file

@ -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);

3
src/pdisksel.c
View file

@ -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;

5
src/pdisksel.h
View file

@ -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);

2
src/pdiskseln.h
View file

@ -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;

12
src/photorec.h
View file

@ -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);

11
src/photorec_check_header.h
View file

@ -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

1
src/poptions.h
View file

@ -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);

3
src/refs.h
View file

@ -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);

1
src/rfs.h
View file

@ -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);

3
src/savehdr.h
View file

@ -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);

8
src/sessionp.h
View file

@ -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);

1
src/sun.h
View file

@ -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);

1
src/swap.h
View file

@ -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);

3
src/sysv.h
View file

@ -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);

1
src/ufs.h
View file

@ -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);

3
src/vmfs.h
View file

@ -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

1
src/xfs.h
View file

@ -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);

1
src/zfs.h
View file

@ -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);