From 1941a27e94a1da627d9f574c03797f131478aadf Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Sun, 8 Oct 2023 14:31:06 +0200
Subject: [PATCH] src/file_fbx.c: fix wrong Frama-C annotations

---
 src/file_fbx.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/file_fbx.c b/src/file_fbx.c
index 60485a65..f1461dff 100644
--- a/src/file_fbx.c
+++ b/src/file_fbx.c
@@ -46,7 +46,8 @@ const file_hint_t file_hint_fbx= {
 /*@
   @ requires valid_file_check_param(file_recovery);
   @ ensures  valid_file_check_result(file_recovery);
-  @ assigns  *file_recovery_new;
+  @ assigns *file_recovery->handle, errno, file_recovery->file_size;
+  @ assigns Frama_C_entropy_source;
   @*/
 static void file_check_fbx(file_recovery_t *file_recovery)
 {