New prototype for recover_HFS()

This commit is contained in:
Christophe Grenier 2020-08-02 10:41:55 +02:00
parent b94f8f8aa2
commit cd98865d99
2 changed files with 23 additions and 3 deletions

View file

@ -55,7 +55,7 @@ int check_HFS(disk_t *disk_car,partition_t *partition,const int verbose)
return 0;
}
int recover_HFS(disk_t *disk_car, const hfs_mdb_t *hfs_mdb,partition_t *partition,const int verbose, const int dump_ind, const int backup)
int recover_HFS(const disk_t *disk_car, const hfs_mdb_t *hfs_mdb,partition_t *partition,const int verbose, const int dump_ind, const int backup)
{
uint64_t part_size;
if(test_HFS(disk_car,hfs_mdb,partition,verbose,dump_ind)!=0)

View file

@ -75,9 +75,29 @@ struct hfs_mdb {
uint32_t drCTFlSize; /* 0x92 bytes in the catalog B-tree */
hfs_extent_rec drCTExtRec; /* 0x96 catalog B-tree's first 3 extents */
} __attribute__ ((gcc_struct, __packed__));
int check_HFS(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_HFS(disk_t *disk_car, partition_t *partition, const int verbose);
/*@
@ requires \valid_read(disk_car);
@ requires \valid_read(hfs_mdb);
@ requires \valid(partition);
@ requires separation: \separated(disk_car, hfs_mdb, partition);
@*/
int test_HFS(const disk_t *disk_car, const hfs_mdb_t *hfs_mdb, const partition_t *partition, const int verbose, const int dump_ind);
int recover_HFS(disk_t *disk_car, const hfs_mdb_t *hfs_mdb,partition_t *partition,const int verbose, const int dump_ind, const int backup);
/*@
@ requires \valid_read(disk_car);
@ requires \valid_read(hfs_mdb);
@ requires \valid(partition);
@ requires separation: \separated(disk_car, hfs_mdb, partition);
@*/
int recover_HFS(const disk_t *disk_car, const hfs_mdb_t *hfs_mdb, partition_t *partition, const int verbose, const int dump_ind, const int backup);
#ifdef __cplusplus
} /* closing brace for extern "C" */