Function OLE_parse_summary_aux

src/file_doc.c:1347–1400

@ @ requires 48 <= dirLen <= 1024*1024; @ requires \valid_read(dataPt + (0 .. dirLen-1)); @ requires \initialized(dataPt + (0 .. dirLen-1)); @ requires \valid(ext); @ requires \valid(title + (0 .. 1024-1)); @ requires \valid(file_time); @ requires valid_string(title); @ requires *ext == \null || valid_read_string(*ext); @ requires separation: \separated(dataPt+(..), ext, title +

  @ assigns *ext, *(title + (0..1023)), *file_time;
  @*/
static void OLE_parse_summary_aux(const char *dataPt, const unsigned int dirLen, const char **ext, char *title, time_t *file_time)
{
  unsigned int pos;
  const unsigned char *udataPt=(const unsigned char *)dataPt;
#ifndef DISABLED_FOR_FRAMAC
  assert(dirLen >= 48 && dirLen<=1024*1024);
#endif
  /*@ assert *ext == \null || valid_read_string(*ext); */
  /*@ assert valid_string(title); */
#ifdef DEBUG_OLE
  dump_log(dataPt, dirLen);
#endif
  /*@ assert \valid_read(udataPt + (0 .. dirLen-1)); */
  if(udataPt[0]!=0xfe || udataPt[1]!=0xff)
    return ;
  pos=get32u(dataPt, 44);
  if(pos > dirLen - 8)
  {
    /*@ assert *ext == \null || valid_read_string(*ext); */
    /*@ assert valid_string(title); */
    return ;
  }
  /*@ assert 0 <= pos <= dirLen - 8; */
  {
    /* PropertySet */
    const unsigned int size=get32u(dataPt, pos);
    if(size <= 8 || size > dirLen || pos + size > dirLen)
    {
      /*@ assert *ext == \null || valid_read_string(*ext); */
      /*@ assert valid_string(title); */
      return ;
    }
    /*@ assert size > 8 && size <= dirLen && pos + size <= dirLen; */

    /*@ assert 0 < dirLen <=1024*1024; */
    /*@ assert \valid_read(dataPt + (0 .. dirLen-1)); */
    /*@ assert pos + size <= dirLen; */
    /*@ assert \valid_read(dataPt + (0 .. pos+size-1)); */
    /*@ assert \valid_read(dataPt + pos + (0 .. size-1)); */

    /*@ assert 0 < dirLen <=1024*1024; */
    /*@ assert \initialized(dataPt + (0 .. dirLen-1)); */
    /*@ assert pos + size <= dirLen; */
    /*@ ghost int small_dirLen = pos + size; */
    /*@ assert small_dirLen <= dirLen; */
    /*@ assert \initialized(dataPt + (0 .. small_dirLen-1)); */

    /*@ assert *ext == \null || valid_read_string(*ext); */
    /*@ assert valid_string(title); */
    OLE_parse_PropertySet(&dataPt[pos], size, ext, title, file_time);
  }
  /*@ assert *ext == \null || valid_read_string(*ext); */
  /*@ assert valid_string(title); */
}

/*@
  @ requires \valid_read(ministream + (0 .. ministream_size-1));