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

---
 src/file_lzh.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/file_lzh.c b/src/file_lzh.c
index 05e4f3af..ce994f09 100644
--- a/src/file_lzh.c
+++ b/src/file_lzh.c
@@ -116,7 +116,7 @@ static void file_rename_level0(file_recovery_t *file_recovery)
   /*@ assert sizeof(struct lzh_level0) + hdr->filename_len <= buffer_size; */
   /*@
     @ loop invariant 0 <= i <= hdr->filename_len;
-    @ loop variant i;
+    @ loop assigns i;
     @*/
   for(i=0; i< hdr->filename_len && fn[i]!=0 && fn[i]!='.'; i++);
   /*@ assert 0 <= i <= hdr->filename_len; */