From c966ee4baac3e6648bddef2a61b63ffa055dfd48 Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Sun, 8 Oct 2023 14:14:51 +0200
Subject: [PATCH] src/file_doc.h: add annotations for file_check_doc_aux()

---
 src/file_doc.h | 1 +
 1 file changed, 1 insertion(+)

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);
   @*/