Function OLE_load_MiniFAT

src/file_doc.c:741–784

@ @ requires \valid(IN); @ requires \valid_read(header); @ requires \valid_read(fat); @ requires 9 == le16(header->uSectorShift) || 12 == le16(header->uSectorShift); @ requires le32(header->csectMiniFat) <= 2048; @ ensures \result!=\null ==> \valid((char *)\result + (0 .. (le32(header->csectMiniFat) << le16(header->uSectorShift)) - 1)); @ ensures \result!=\null ==> \initialized((char

  @ ensures \result!=\null ==> \initialized((char *)\result + (0 .. (le32(header->csectMiniFat) << le16(header->uSectorShift)) - 1));
  @*/
static uint32_t *OLE_load_MiniFAT(FILE *IN, const struct OLE_HDR *header, const uint32_t *fat, const unsigned int fat_entries, const uint64_t offset)
{
  char *minifat;
  unsigned int block;
  unsigned int i;
  const unsigned int uSectorShift=le16(header->uSectorShift);
  const unsigned int csectMiniFat=le32(header->csectMiniFat);
  /*@ assert uSectorShift==9 || uSectorShift==12; */
  /*@ assert csectMiniFat <= 2048; */
  const unsigned int minifat_length=csectMiniFat << uSectorShift;
  if(csectMiniFat==0)
    return NULL;
  /*@ assert 0 < csectMiniFat; */
  /*@ assert 0 < csectMiniFat <= 2048; */
#ifdef DISABLED_FOR_FRAMAC
  minifat=(char *)MALLOC(2048 << 12);
#else
  minifat=(char *)MALLOC(minifat_length);
#endif
  block=le32(header->MiniFat_block);
  /*@
    @ loop invariant 0 <= i <= csectMiniFat;
    @ loop invariant i > 0 ==> \initialized(minifat + ((i-1)<<uSectorShift) + (0 .. (1<<uSectorShift)- 1));
    @ loop invariant i > 0 ==> \initialized(minifat + (0 .. (i<<uSectorShift)- 1));
    @ loop variant csectMiniFat-i;
    @*/
  for(i=0; i < csectMiniFat; i++)
  {
    if(block >= fat_entries)
    {
      free(minifat);
      return NULL;
    }
    if(OLE_read_block(IN, minifat + (i << uSectorShift), uSectorShift, block, offset)<0)
    {
      free(minifat);
      return NULL;
    }
    block=le32(fat[block]);
  }
  /*@ assert \initialized(minifat + (0 .. (csectMiniFat<<uSectorShift)- 1)); */
  /*@ assert \initialized(minifat + (0 .. (le32(header->csectMiniFat) << le16(header->uSectorShift))- 1)); */
  return (uint32_t *)minifat;
}

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