Function OLE_parse_title_entry

src/file_doc.c:1082–1136

@ @ requires 8 <= size <= 1024*1024; @ requires offset <= size; @ requires \valid_read(buffer+ (0 .. size-1)); @ requires \valid(title + (0 .. 1024-1)); @ requires valid_string(title); @ requires \initialized(buffer+ (0 .. size-1)); @ ensures valid_string(title); @ assigns *(title + (0 .. 1023)); @*/

  @ assigns *(title + (0 .. 1023));
  @*/
static void OLE_parse_title_entry(const char *buffer, const unsigned int size, const unsigned int offset, char *title)
{
  if(offset + 8 > size)
  {
    return;
  }
  /*@ assert offset + 8 <= size; */
  {
    /*@ assert \valid_read(buffer + (0 .. size - 1)); */
    const unsigned int count=get32u(buffer, offset + 4);
    const unsigned int offset_tmp=offset + 8;
    const char *src=(const char *)buffer;
    if(count <= 1 || count > size)
    {
      return;
    }
    /*@ assert 1 < count <= size; */
    /*@ assert 1 < count <= 1024*1024; */
    if(offset_tmp + count > size)
    {
      return;
    }
    /*@ assert offset_tmp + count <= size; */
    /*@ assert \valid_read(src + (0 .. size - 1)); */
    /*@ assert offset_tmp + count <= size; */
    /*@ assert \valid_read(src + (0 .. offset_tmp + count - 1)); */
    /*@ assert \valid_read((src + offset_tmp) + (0 .. count - 1)); */
    /*@ assert \valid_read((src + offset_tmp) + (1 .. count - 1)); */
    /*@ assert \valid_read((char*)src + (0 .. offset_tmp + count - 1)); */
    /*@ assert \valid_read(((char*)(src+offset_tmp))+(0..count-1)); */
    /*@ assert \valid_read(((char*)(src+offset_tmp))+(1..count-1)); */
    /*@ assert \valid_read((char*)(src + offset_tmp)); */
    /*@ assert \valid_read((char*)(src + offset_tmp)) && \valid_read(((char*)(src+offset_tmp))+(1..count-1)); */
    /*@ assert valid_read_or_empty((void const *)(src + offset_tmp), count); */
    /*@ assert valid_read_or_empty((void const *)(src + offset_tmp), count); */
#ifndef DISABLED_FOR_FRAMAC
    if(count < 1024)
    {
      memcpy(title, &src[offset_tmp], count);
      title[count]='\0';
      /*@ assert valid_string(title); */
    }
    else
    {
      memcpy(title, &src[offset_tmp], 1023);
      title[1023]='\0';
      /*@ assert valid_string(title); */
    }
#endif
#ifdef DEBUG_OLE
    log_info("Title %s\n", title);
#endif
  }
  /*@ assert valid_string(title); */
}

/*@
  @ requires 8 <= size <= 1024*1024;