Function VerifyBlock

src/apfs_common.c:67–76

@ @ requires size >= 8; @ requires \valid_read((char *)block+ (0 .. size-1)); @ assigns \nothing; @*/

  @ assigns  \nothing;
  @*/
static uint64_t VerifyBlock(const void *block, const size_t size)
{
  uint64_t cs;
  const uint32_t *data = (const uint32_t *)block;
  const size_t size4 = size / sizeof(uint32_t);

  cs = fletcher64(data + 2, size4 - 2, 0);
  cs = fletcher64(data, 2, cs);
  return cs;
}

int test_APFS(const nx_superblock_t *sb, const partition_t *partition)
{