Function get32u

src/file_doc.c:792–802

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

  @ assigns \nothing;
  @*/
static uint32_t get32u(const void *buffer, const unsigned int offset)
{
  /*@ assert \valid_read((char *)buffer + offset + (0 .. 4-1)); */
  /*@ assert \initialized((char *)buffer + offset + (0 .. 4-1)); */
  const char *ptr=(const char *)buffer+offset;
  /*@ assert \valid_read(ptr + (0 .. 4-1)); */
  /*@ assert \initialized(ptr + (0 .. 4-1)); */
  const uint32_t *val=(const uint32_t *)ptr;
  /*@ assert \valid_read(val); */
  return le32(*val);
}

/*@
  @ requires \valid_read((char *)buffer + (offset .. offset + 8 - 1));