diff options
Diffstat (limited to 'src/dimage.h')
| -rw-r--r-- | src/dimage.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/dimage.h b/src/dimage.h index ac304d24..1b588b2f 100644 --- a/src/dimage.h +++ b/src/dimage.h @@ -25,6 +25,13 @@ extern "C" { #endif +/*@ + @ requires \valid(disk_car); + @ requires valid_disk(disk_car); + @ requires \valid_read(partition); + @ requires valid_read_string(image_dd); + @ requires \separated(disk_car, partition, image_dd); + @*/ int disk_image(disk_t *disk_car, const partition_t *partition, const char *image_dd); #ifdef __cplusplus |