diff options
Diffstat (limited to 'src/photorec.h')
| -rw-r--r-- | src/photorec.h | 176 |
1 files changed, 171 insertions, 5 deletions
diff --git a/src/photorec.h b/src/photorec.h index 7b3345df..84cbb503 100644 --- a/src/photorec.h +++ b/src/photorec.h @@ -64,61 +64,227 @@ struct ph_param uint64_t offset; }; +/*@ + predicate valid_ph_param(struct ph_param *p) = (\valid_read(p) && + (p->recup_dir == \null || valid_read_string(p->recup_dir)) + ); + @*/ + +#define PH_INVALID_OFFSET 0xffffffffffffffff + +/*@ + @ requires valid_list_search_space(list_search_space); + @ requires \separated(list_search_space, current_search_space, offset); + @ requires current_search_space==\null || (\valid(*current_search_space) && valid_list_search_space(*current_search_space)); + @ ensures \result==0 ==> (*current_search_space!=list_search_space && *offset == (*current_search_space)->start); + @*/ +// ensures current_search_space==\null || (\valid(*current_search_space) && valid_list_search_space(*current_search_space)); int get_prev_file_header(const alloc_data_t *list_search_space, alloc_data_t **current_search_space, uint64_t *offset); + +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_recovery, params, list_search_space); + @*/ int file_finish_bf(file_recovery_t *file_recovery, struct ph_param *params, alloc_data_t *list_search_space); + +/*@ + @ requires \valid(file_recovery); + @ requires valid_file_recovery(file_recovery); + @ requires valid_list_search_space(list_search_space); + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \separated(file_recovery, params, list_search_space, &errno); + @*/ void file_recovery_aborted(file_recovery_t *file_recovery, struct ph_param *params, alloc_data_t *list_search_space); /*@ @ requires \valid(file_recovery); + @ requires valid_file_recovery(file_recovery); @ requires \valid(params); - @ requires \valid(list_search_space); - @ ensures \result == PFSTATUS_BAD || \result == PFSTATUS_OK || \result == PFSTATUS_OK_TRUNCATED; + @ requires valid_ph_param(params); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_recovery, params, list_search_space); + @ ensures \result == PFSTATUS_BAD || \result == PFSTATUS_OK || \result == PFSTATUS_OK_TRUNCATED; @*/ +// ensures valid_file_recovery(file_recovery); pfstatus_t file_finish2(file_recovery_t *file_recovery, struct ph_param *params, const int paranoid, alloc_data_t *list_search_space); +/*@ + @ requires \valid_read(file_stats); + @*/ void write_stats_log(const file_stat_t *file_stats); + +/*@ + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_stats, list_search_space); + @*/ +//ensures valid_list_search_space(list_search_space); void update_stats(file_stat_t *file_stats, alloc_data_t *list_search_space); +/*@ + @ requires \valid_read(disk_car); + @ requires valid_disk(disk_car); + @*/ +// ensures valid_partition(\result); partition_t *new_whole_disk(const disk_t *disk_car); -unsigned int find_blocksize(alloc_data_t *list_file, const unsigned int default_blocksize, uint64_t *offset); + +/*@ + @ requires valid_list_search_space(list_file); + @ requires \valid(offset); + @ requires \separated(list_file, offset); + @ requires default_blocksize > 0; + @*/ +// ensures \result > 0; +unsigned int find_blocksize(const alloc_data_t *list_file, const unsigned int default_blocksize, uint64_t *offset); + +/*@ + @ requires blocksize > 0; + @ requires valid_list_search_space(list_search_space); + @*/ void update_blocksize(const unsigned int blocksize, alloc_data_t *list_search_space, const uint64_t offset); + +/*@ + @ requires valid_list_search_space(list_search_space); + @ requires current_search_space==\null || valid_list_search_space(current_search_space); + @*/ +// ensures current_search_space==\null || valid_list_search_space(current_search_space); void forget(const alloc_data_t *list_search_space, alloc_data_t *current_search_space); /*@ - @ requires \valid(list_search_space); + @ requires valid_list_search_space(list_search_space); @ requires \valid_read(disk_car); + @ requires valid_disk(disk_car); @ requires disk_car->disk_size > 0; @ requires disk_car->disk_real_size > 0; @ requires \valid_read(partition); @ requires separation: \separated(list_search_space, disk_car, partition); @*/ void init_search_space(alloc_data_t *list_search_space, const disk_t *disk_car, const partition_t *partition); + +/*@ + @ requires valid_disk(disk_car); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(disk_car, partition, list_search_space); + @ ensures valid_list_search_space(list_search_space); + @ ensures valid_disk(disk_car); + @ ensures valid_list_search_space(list_search_space); + @*/ unsigned int remove_used_space(disk_t *disk_car, const partition_t *partition, alloc_data_t *list_search_space); + +/*@ + @ requires valid_list_search_space(list_search_space); + @*/ void free_list_search_space(alloc_data_t *list_search_space); + int sorfile_stat_ts(const void *p1, const void *p2); + +/*@ + @ requires valid_read_string(recup_dir); + @ requires \separated(recup_dir, &errno); + @*/ unsigned int photorec_mkdir(const char *recup_dir, const unsigned int initial_dir_num); + +/*@ + @ requires valid_list_search_space(list_search_space); + @ requires \separated(list_search_space, current_search_space); + @ ensures valid_list_search_space(list_search_space); + @*/ void info_list_search_space(const alloc_data_t *list_search_space, const alloc_data_t *current_search_space, const unsigned int sector_size, const int keep_corrupted_file, const int verbose); + +/*@ + @ requires valid_list_search_space(list_search_space); + @*/ void free_search_space(alloc_data_t *list_search_space); + +/*@ + @ requires \valid(file_recovery); + @ requires valid_file_recovery(file_recovery); + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \separated(file_recovery, params); + @*/ +// ensures valid_file_recovery(file_recovery); void set_filename(file_recovery_t *file_recovery, struct ph_param *params); + +/*@ + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(params, new_current_search_space, list_search_space); + @ requires new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); + @*/ +// ensures new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); +// ensures valid_list_search_space(list_search_space); uint64_t set_search_start(struct ph_param *params, alloc_data_t **new_current_search_space, alloc_data_t *list_search_space); + +/*@ + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \valid_read(options); + @ requires \separated(params, options); + @*/ void params_reset(struct ph_param *params, const struct ph_options *options); + +/*@ + @ assigns \nothing; + @*/ const char *status_to_name(const photorec_status_t status); + +/*@ + @ requires \valid(params); + @ requires valid_ph_param(params); + @ requires \valid_read(options); + @ requires \separated(params, options); + @ assigns params->offset, params->status, params->file_nbr; + @*/ void status_inc(struct ph_param *params, const struct ph_options *options); /*@ @ requires \valid(disk); + @ requires valid_disk(disk); @ requires \valid_read(&disk->arch); @ requires \valid_function(disk->arch->read_part); @ requires \valid_read(options); + @ requires \separated(disk, options); + @ ensures valid_disk(disk); @*/ +// ensures valid_list_part(\result); list_part_t *init_list_part(disk_t *disk, const struct ph_options *options); + +/*@ + @ requires valid_file_recovery(file_recovery); + @*/ +// ensures valid_file_recovery(file_recovery); void file_block_log(const file_recovery_t *file_recovery, const unsigned int sector_size); -void file_block_free(alloc_list_t *list_allocation); + +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_recovery, list_search_space, new_current_search_space, offset); + @ requires new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); + @*/ +// ensures new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); +// ensures valid_file_recovery(file_recovery); +// ensures valid_list_search_space(list_search_space); void file_block_append(file_recovery_t *file_recovery, alloc_data_t *list_search_space, alloc_data_t **new_current_search_space, uint64_t *offset, const unsigned int blocksize, const unsigned int data); + +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires valid_list_search_space(list_search_space); + @ requires \separated(file_recovery, list_search_space, new_current_search_space, offset, buffer + (..)); + @ requires new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); + @*/ +// ensures new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space)); +// ensures valid_file_recovery(file_recovery); +// ensures valid_list_search_space(list_search_space); void file_block_truncate_and_move(file_recovery_t *file_recovery, alloc_data_t *list_search_space, const unsigned int blocksize, alloc_data_t **new_current_search_space, uint64_t *offset, unsigned char *buffer); /*@ @ requires \valid(list_search_space); + @ requires valid_list_search_space(list_search_space); @*/ void del_search_space(alloc_data_t *list_search_space, const uint64_t start, const uint64_t end); |