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

src/crc.c: fix Frama-C annotations for get_crc32

Browse source
This commit is contained in:
Christophe Grenier 2023-10-08 13:56:32 +02:00
parent d29facb0d7
commit 28e29554f7
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/crc.c
View file

@ -90,6 +90,7 @@ unsigned int get_crc32(const void*buf, const unsigned int len, const uint32_t se
unsigned int i; unsigned int i;
register uint32_t crc32val; register uint32_t crc32val;
const unsigned char *s=(const unsigned char *)buf; const unsigned char *s=(const unsigned char *)buf;
/*@ assert \valid_read(s + (0 .. len-1)); */
crc32val = seed; crc32val = seed;
/*@ loop invariant 0 <= i <= len; /*@ loop invariant 0 <= i <= len;
@ loop assigns i, crc32val; */ @ loop assigns i, crc32val; */