diff options
Diffstat (limited to 'src/exfat.c')
| -rw-r--r-- | src/exfat.c | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/exfat.c b/src/exfat.c index dac6e743..8aef7854 100644 --- a/src/exfat.c +++ b/src/exfat.c @@ -50,6 +50,11 @@ int exfat_read_cluster(disk_t *disk, const partition_t *partition, const struct partition->part_offset + exfat_cluster_to_offset(exfat_header, cluster)); } +/*@ + @ requires \valid(partition); + @ requires \valid_read(exfat_header); + @ requires \separated(partition, exfat_header); + @*/ static void set_exFAT_info(partition_t *partition, const struct exfat_super_block*exfat_header) { partition->upart_type=UP_EXFAT; |