luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

src/file_lzh.c: fix wrong Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2023-10-08 14:40:17 +02:00
parent 73411e2f6d
commit 8582846b9b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/file_lzh.c
View file

@ -116,7 +116,7 @@ static void file_rename_level0(file_recovery_t *file_recovery)
/*@ assert sizeof(struct lzh_level0) + hdr->filename_len <= buffer_size; */ /*@ assert sizeof(struct lzh_level0) + hdr->filename_len <= buffer_size; */
/*@ /*@
@ loop invariant 0 <= i <= hdr->filename_len; @ 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++); for(i=0; i< hdr->filename_len && fn[i]!=0 && fn[i]!='.'; i++);
/*@ assert 0 <= i <= hdr->filename_len; */ /*@ assert 0 <= i <= hdr->filename_len; */