Function OLE_read_stream

src/file_doc.c:687–730

@ @ requires \valid(IN); @ requires \valid_read(fat + (0 .. fat_entries-1)); @ requires 9 == uSectorShift || 12 == uSectorShift; @ requires 0 < len <= 1024*1024; @ requires \separated(IN, fat + (..), &errno, &Frama_C_entropy_source); @ ensures \result!=\null ==> \valid((char *)\result + (0 .. len - 1)); @ ensures \result!=\null ==> \initialized((char *)\result + (0 .. len - 1)); @*

  @ ensures \result!=\null ==> \initialized((char *)\result + (0 .. len - 1));
  @*/
static void *OLE_read_stream(FILE *IN,
    const uint32_t *fat, const unsigned int fat_entries, const unsigned int uSectorShift,
    const unsigned int block_start, const unsigned int len, const uint64_t offset)
{
  //@ split uSectorShift;
  char *dataPt;
  unsigned int block;
  unsigned int i;
  /*@ assert 9 == uSectorShift || 12 == uSectorShift; */
  const unsigned int i_max=((len+(1<<uSectorShift)-1) >> uSectorShift);
#ifdef DISABLED_FOR_FRAMAC
  dataPt=(char *)MALLOC(((1024*1024+(1<<uSectorShift)-1) >> uSectorShift) << uSectorShift);
#else
  dataPt=(char *)MALLOC(i_max << uSectorShift);
#endif
  /*@ assert \valid(dataPt + ( 0 .. len-1)); */
  /*@
    @ loop invariant 0 <= i <= i_max;
    @ loop invariant i > 0 ==> \initialized(dataPt + ((i-1)<<uSectorShift) + (0 .. (1<<uSectorShift)- 1));
    @ loop invariant i > 0 ==> \initialized(dataPt + (0 .. (i<<uSectorShift)- 1));
    @ loop variant i_max - i;
    @*/
  for(i=0, block=block_start;
      i < i_max;
      i++, block=le32(fat[block]))
  {
    if(!(block < fat_entries))
    {
      free(dataPt);
      return NULL;
    }
    if(OLE_read_block(IN, &dataPt[i<<uSectorShift], uSectorShift, block, offset)<0)
    {
      free(dataPt);
      return NULL;
    }
    /*@ assert \initialized(dataPt + ((i<<uSectorShift) .. (i<<uSectorShift) + (1<<uSectorShift)- 1)); */
    /*@ assert \initialized(dataPt + (i<<uSectorShift) + (0 .. (1<<uSectorShift)- 1)); */
  }
  /*@ assert \initialized(dataPt + (0 .. (i_max<<uSectorShift)- 1)); */
  /*@ assert \initialized(dataPt + (0 .. len - 1)); */
  /*@ assert \valid(dataPt + (0 .. len - 1)); */
  return dataPt;
}

/*@
  @ requires \valid(IN);