src/file_doc.h: Add missing annotations from commit ac8fe16518
This commit is contained in:
parent
872bd3fafe
commit
03d1688d79
1 changed files with 4 additions and 0 deletions
|
@ -25,6 +25,10 @@
|
||||||
extern "C" {
|
extern "C" {
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
/*@
|
||||||
|
@ requires valid_file_check_param(file_recovery);
|
||||||
|
@ ensures valid_file_check_result(file_recovery);
|
||||||
|
@*/
|
||||||
void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset);
|
void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset);
|
||||||
|
|
||||||
#ifdef __cplusplus
|
#ifdef __cplusplus
|
||||||
|
|
Loading…
Reference in a new issue