diff --git a/src/file_doc.h b/src/file_doc.h
index a58a9103..757028a4 100644
--- a/src/file_doc.h
+++ b/src/file_doc.h
@@ -26,6 +26,7 @@ extern "C" {
 #endif
 
 /*@
+  @ requires offset <= 4006;
   @ requires valid_file_check_param(file_recovery);
   @ ensures  valid_file_check_result(file_recovery);
   @*/