diff options
Diffstat (limited to 'src/btrfs.h')
| -rw-r--r-- | src/btrfs.h | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/btrfs.h b/src/btrfs.h index dad5511f..022c6962 100644 --- a/src/btrfs.h +++ b/src/btrfs.h @@ -140,7 +140,20 @@ struct btrfs_super_block { uint8_t sys_chunk_array[BTRFS_SYSTEM_CHUNK_ARRAY_SIZE]; } __attribute__ ((gcc_struct, __packed__)); -int check_btrfs(disk_t *disk_car,partition_t *partition); +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid(partition); + @ requires \separated(disk_car, partition); + @*/ +int check_btrfs(disk_t *disk_car, partition_t *partition); + +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid(partition); + @ requires \separated(disk_car, sb, partition); + @*/ int recover_btrfs(const disk_t *disk_car, const struct btrfs_super_block *sb,partition_t *partition,const int verbose, const int dump_ind); #ifdef __cplusplus |