diff options
Diffstat (limited to 'src/fat1x.h')
| -rw-r--r-- | src/fat1x.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/fat1x.h b/src/fat1x.h index 1c933ca0..852c5c07 100644 --- a/src/fat1x.h +++ b/src/fat1x.h @@ -25,6 +25,12 @@ extern "C" { #endif +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid(partition); + @ requires \separated(disk_car, partition); + @*/ int fat1x_boot_sector(disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind, const unsigned int expert, char **current_cmd); #ifdef __cplusplus |