src/file_doc.h: add annotations for file_check_doc_aux()
This commit is contained in:
parent
d90b4571d7
commit
c966ee4baa
1 changed files with 1 additions and 0 deletions
|
@ -26,6 +26,7 @@ extern "C" {
|
|||
#endif
|
||||
|
||||
/*@
|
||||
@ requires offset <= 4006;
|
||||
@ requires valid_file_check_param(file_recovery);
|
||||
@ ensures valid_file_check_result(file_recovery);
|
||||
@*/
|
||||
|
|
Loading…
Reference in a new issue