diff options
Diffstat (limited to 'src/autoset.h')
| -rw-r--r-- | src/autoset.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/autoset.h b/src/autoset.h index 9dccbeb2..a7f512bf 100644 --- a/src/autoset.h +++ b/src/autoset.h @@ -27,6 +27,7 @@ extern "C" { /*@ @ requires \valid(disk_car); + @ requires valid_disk(disk_car); @ assigns disk_car->unit; @*/ void autoset_unit(disk_t *disk_car); |