Function OLE_read_ministream

src/file_doc.c:1412–1456

@ @ requires \valid_read(ministream + (0 .. ministream_size-1)); @ requires \valid_read(minifat + (0 .. minifat_entries-1)); @ requires \initialized(ministream + (0 .. ministream_size-1)); @ requires \initialized(minifat + (0 .. minifat_entries-1)); @ requires uMiniSectorShift==6; @ requires 48 <= len <= 1024*1024; @ ensures \result!=\null ==> \valid((char *)\result + (0 .. len-1));

  @ ensures \result!=\null ==> \initialized((char *)\result + (0 .. len-1));
  @*/
static void *OLE_read_ministream(const unsigned char *ministream,
    const uint32_t *minifat, const unsigned int minifat_entries, const unsigned int uMiniSectorShift,
    const unsigned int miniblock_start, const unsigned int len, const unsigned int ministream_size)
{
  unsigned char *dataPt;
  unsigned int mblock=miniblock_start;
  unsigned int size_read;
  /*@ assert uMiniSectorShift==6; */
#ifdef DISABLED_FOR_FRAMAC
  const unsigned int len_aligned=(1024*1024+(1<<uMiniSectorShift)-1) / (1<<uMiniSectorShift) * (1<<uMiniSectorShift);
#else
  const unsigned int len_aligned=(len+(1<<uMiniSectorShift)-1) / (1<<uMiniSectorShift) * (1<<uMiniSectorShift);
#endif
  dataPt=(unsigned char *)MALLOC(len_aligned);
  /*@
    @ loop invariant uMiniSectorShift==6;
    @ loop invariant 48 <= len <= 1024*1024;
    @ loop invariant 0 <= size_read < len + (1<<uMiniSectorShift);
    @ loop invariant size_read > 0 ==> \initialized(dataPt + size_read - (1<<uMiniSectorShift) + (0 .. (1<<uMiniSectorShift)- 1));
    @ loop invariant size_read > 0 ==> \initialized(dataPt + (0 .. size_read - 1));
    @ loop variant len - size_read;
    @*/
  for(size_read=0;
      size_read < len;
      size_read+=(1<<uMiniSectorShift))
  {
    if(mblock >= minifat_entries)
    {
      free(dataPt);
      return NULL;
    }
    if(mblock >= ministream_size>>uMiniSectorShift)
    {
      free(dataPt);
      return NULL;
    }
    /*@ assert mblock < ministream_size>>uMiniSectorShift; */
    memcpy(&dataPt[size_read], &ministream[mblock<<uMiniSectorShift], (1<<uMiniSectorShift));
    /*@ assert \initialized(dataPt + size_read + (0 .. (1<<uMiniSectorShift)-1)); */
    /*@ assert \valid_read(minifat + mblock); */
    mblock=le32(minifat[mblock]);
  }
  /*@ assert \initialized(dataPt + (0 .. len - 1)); */
  return dataPt;
}

/*@
  @ requires \valid(file);