diff --git a/src/file_doc.h b/src/file_doc.h index 2c5e0ba6..a58a9103 100644 --- a/src/file_doc.h +++ b/src/file_doc.h @@ -25,6 +25,10 @@ extern "C" { #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); #ifdef __cplusplus