From 9c37fccbd38ec9549668aa9edf72df9dfb1ebc41 Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Sun, 8 Oct 2023 14:11:47 +0200
Subject: [PATCH] src/apfs_common.c: fix Frama-C annotations for fletcher64()

---
 src/apfs_common.c | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/apfs_common.c b/src/apfs_common.c
index 57ab9c31..fda17ec1 100644
--- a/src/apfs_common.c
+++ b/src/apfs_common.c
@@ -36,7 +36,7 @@
 #include "log.h"
 
 /*@
-  @ requires \valid_read((char *)data + (0 .. cnt-1));
+  @ requires \valid_read(data + (0 .. cnt-1));
   @ assigns  \nothing;
   @*/
 static uint64_t fletcher64(const uint32_t *data, const size_t cnt, const uint64_t init)
@@ -44,9 +44,13 @@ static uint64_t fletcher64(const uint32_t *data, const size_t cnt, const uint64_
   size_t k;
   uint64_t sum1 = init & 0xFFFFFFFFU;
   uint64_t sum2 = (init >> 32);
-  /*@ loop assigns k, sum1, sum2; */
+  /*@
+    @ loop invariant 0 <= k <= cnt;
+    @ loop assigns k, sum1, sum2;
+    @*/
   for (k = 0; k < cnt; k++)
   {
+    /* @assert k < cnt; */
     sum1 = (sum1 + le32(data[k]));
     sum2 = (sum2 + sum1);
   }
@@ -56,6 +60,7 @@ static uint64_t fletcher64(const uint32_t *data, const size_t cnt, const uint64_
 }
 
 /*@
+  @ requires size >= 8;
   @ requires \valid_read((char *)block+ (0 .. size-1));
   @ assigns  \nothing;
   @*/