Function get64u

src/file_doc.c:810–818

@ @ requires \valid_read((char *)buffer + (offset .. offset + 8 - 1)); @ requires \initialized((char *)buffer + (offset .. offset + 8 - 1)); @ terminates \true; @ assigns \nothing; @*/

  @ assigns \nothing;
  @*/
static uint64_t get64u(const void *buffer, const unsigned int offset)
{
  /*@ assert \valid_read((char *)(buffer + offset) + (0 .. 7)); */
  const char *ptr=(const char *)buffer + offset;
  /*@ assert \valid_read(ptr + (0 .. 7)); */
  const uint64_t *val=(const uint64_t *)ptr;
  /*@ assert \valid_read(val); */
  return le64(*val);
}

/*@
  @ requires \valid(ext);