@ @ requires \valid_read(data + (0 .. cnt-1)); @ assigns \nothing; @*/
| 40 | @ assigns \nothing; |
| 41 | @*/ |
| 42 | static uint64_t fletcher64(const uint32_t *data, const size_t cnt, const uint64_t init) |
| 43 | { |
| 44 | size_t k; |
| 45 | uint64_t sum1 = init & 0xFFFFFFFFU; |
| 46 | uint64_t sum2 = (init >> 32); |
| 47 | /*@ |
| 48 | @ loop invariant 0 <= k <= cnt; |
| 49 | @ loop assigns k, sum1, sum2; |
| 50 | @*/ |
| 51 | for (k = 0; k < cnt; k++) |
| 52 | { |
| 53 | /* @assert k < cnt; */ |
| 54 | sum1 = (sum1 + le32(data[k])); |
| 55 | sum2 = (sum2 + sum1); |
| 56 | } |
| 57 | sum1 = sum1 % 0xFFFFFFFF; |
| 58 | sum2 = sum2 % 0xFFFFFFFF; |
| 59 | return (sum2 << 32) | sum1; |
| 60 | } |
| 61 | |
| 62 | /*@ |
| 63 | @ requires size >= 8; |