Function OLE_read_block

src/file_doc.c:101–121

@ @ requires \valid(IN); @ requires (9 == uSectorShift) || (12 == uSectorShift); @ requires \valid( buf + (0 .. (1< \initialized(buf + (0 .. (1<<uSectorShift)-1)); @ assigns *IN, errno; @ assigns *((char *)buf + (0

  @ assigns Frama_C_entropy_source;
  @*/
static int OLE_read_block(FILE *IN, char *buf, const unsigned int uSectorShift, const unsigned int block, const uint64_t offset)
{
  const size_t size=1<<uSectorShift;
  /*@ assert size == 1<<uSectorShift; */
  if(block==0xFFFFFFFF || block==0xFFFFFFFE)
    return -1;
  if(my_fseek(IN, offset + ((uint64_t)(1+block)<<uSectorShift), SEEK_SET) < 0)
  {
    return -1;
  }
  if(fread(buf, size, 1, IN)!=1)
  {
    return -1;
  }
#if defined(__FRAMAC__)
  Frama_C_make_unknown(buf, size);
#endif
  /*@ assert \initialized(buf + (0 .. size-1)); */
  /*@ assert \initialized(buf + (0 .. (1<<uSectorShift)-1)); */
  return 0;
}

/*@
  @ requires \valid(IN);