summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-08-30 11:05:35 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-08-30 11:05:35 +0200
commite9716150a10f94f92c1aea47ceeb30080baf01e6 (patch)
treed67b9b1e58b347c48013e875d4f46cb67abc3b55
parent208ee976f7ec71f8a00ed7dec8a9518d161ce697 (diff)
crc.[ch]: fix frama-c annotations
-rw-r--r--src/crc.c2
-rw-r--r--src/crc.h1
2 files changed, 2 insertions, 1 deletions
diff --git a/src/crc.c b/src/crc.c
index 58a01e6..10dd8bd 100644
--- a/src/crc.c
+++ b/src/crc.c
@@ -91,7 +91,7 @@ unsigned int get_crc32(const void*buf, const unsigned int len, const uint32_t se
register uint32_t crc32val;
const unsigned char *s=(const unsigned char *)buf;
crc32val = seed;
- /*@ loop assigns crc32val; */
+ /*@ loop assigns i, crc32val; */
for (i = 0; i < len; i ++)
{
crc32val = crc32_tab[(crc32val ^ s[i]) & 0xff] ^ (crc32val >> 8);
diff --git a/src/crc.h b/src/crc.h
index b49084b..846fa14 100644
--- a/src/crc.h
+++ b/src/crc.h
@@ -30,6 +30,7 @@ unsigned int get_crc32_gen(const unsigned char *s, const unsigned int len, const
#endif
/*@
@ requires \valid_read((const char *)s + (0 .. len-1));
+ @ requires \initialized((const char *)s + (0 .. len-1));
@ assigns \nothing;
@*/
unsigned int get_crc32(const void *s, const unsigned int len, const uint32_t seed);