From 28e29554f79dd9cbac0aafdfc2425841b40edfaf Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Sun, 8 Oct 2023 13:56:32 +0200
Subject: [PATCH] src/crc.c: fix Frama-C annotations for get_crc32

---
 src/crc.c | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/crc.c b/src/crc.c
index 62bb3c80..8c8418a8 100644
--- a/src/crc.c
+++ b/src/crc.c
@@ -90,6 +90,7 @@ unsigned int get_crc32(const void*buf, const unsigned int len, const uint32_t se
   unsigned int i;
   register uint32_t crc32val;
   const unsigned char *s=(const unsigned char *)buf;
+  /*@ assert \valid_read(s + (0 .. len-1)); */
   crc32val = seed; 
   /*@ loop invariant 0 <= i <= len;
     @ loop assigns i, crc32val; */