diff options
Diffstat (limited to 'src/cramfs.h')
| -rw-r--r-- | src/cramfs.h | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/cramfs.h b/src/cramfs.h index dc126957..eef22aae 100644 --- a/src/cramfs.h +++ b/src/cramfs.h @@ -84,7 +84,21 @@ struct cramfs_super { }; +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid(partition); + @ requires \separated(disk_car, partition); + @*/ int check_cramfs(disk_t *disk_car,partition_t *partition,const int verbose); + +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid(partition); + @ requires \separated(disk_car, partition, sb); + @ requires \valid_read(sb); + @*/ int recover_cramfs(const disk_t *disk_car, const struct cramfs_super *sb, partition_t *partition, const int verbose, const int dump_ind); #ifdef __cplusplus |