diff options
| author | Christophe Grenier <[email protected]> | 2021-11-20 11:26:50 +0100 |
|---|---|---|
| committer | Christophe Grenier <[email protected]> | 2021-11-20 11:26:50 +0100 |
| commit | b2a0d41da609e62865beec1ed6faddd12bb5bdb8 (patch) | |
| tree | 2312b72445a9bce2e2c4790fb088d24bc030e90c /src/f2fs.h | |
| parent | edcb650063911b563486bbbc54d62810145ca58b (diff) | |
Numerous frama-c annotations
Diffstat (limited to 'src/f2fs.h')
| -rw-r--r-- | src/f2fs.h | 18 |
1 files changed, 18 insertions, 0 deletions
@@ -25,8 +25,26 @@ extern "C" { #endif +/*@ + @ requires \valid(disk); + @ requires valid_disk(disk); + @ requires \valid(partition); + @ requires \separated(disk, partition); + @*/ int check_f2fs(disk_t *disk, partition_t *partition); + +/*@ + @ requires \valid_read(hdr); + @*/ int test_f2fs(const struct f2fs_super_block *hdr); + +/*@ + @ requires \valid(disk); + @ requires valid_disk(disk); + @ requires \valid_read(hdr); + @ requires \valid(partition); + @ requires \separated(disk, hdr, partition); + @*/ int recover_f2fs(const disk_t *disk, const struct f2fs_super_block *hdr, partition_t *partition); #ifdef __cplusplus |