diff options
Diffstat (limited to 'src/fat_cluster.h')
| -rw-r--r-- | src/fat_cluster.h | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/src/fat_cluster.h b/src/fat_cluster.h index 9bc53fea..df818a66 100644 --- a/src/fat_cluster.h +++ b/src/fat_cluster.h @@ -42,9 +42,29 @@ struct cluster_offset_struct unsigned int first_sol; }; +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid_read(partition); + @ requires valid_partition(partition); + @ requires \valid(sectors_per_cluster); + @ requires \valid(offset); + @ requires \separated(disk_car, partition, sectors_per_cluster, offset); + @*/ 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); + +/*@ + @ assigns \nothing; + @*/ upart_type_t no_of_cluster2part_type(const unsigned long int no_of_cluster); -int find_sectors_per_cluster_aux(const sector_cluster_t *sector_cluster, const unsigned int nbr_sector_cluster,unsigned int *sectors_per_cluster, uint64_t *offset, const int verbose, const unsigned long int part_size_in_sectors, const upart_type_t upart_type); + +/*@ + @ requires \valid_read(sector_cluster + (0 .. nbr_sector_cluster-1)); + @ requires \valid(sectors_per_cluster); + @ requires \valid(offset); + @ requires \separated(sector_cluster + (..), sectors_per_cluster, offset); + @*/ +int find_sectors_per_cluster_aux(const sector_cluster_t *sector_cluster, const unsigned int nbr_sector_cluster, unsigned int *sectors_per_cluster, uint64_t *offset, const int verbose, const unsigned long int part_size_in_sectors, const upart_type_t upart_type); #ifdef __cplusplus } /* closing brace for extern "c" */ |