Function OLE_parse_uni_software_entry

src/file_doc.c:1022–1070

@ @ requires 8 <= size <= 1024*1024; @ requires offset <= size; @ requires \valid_read(buffer+ (0 .. size-1)); @ requires \initialized(buffer+ (0 .. size-1)); @ requires \valid(ext); @ requires *ext == \null || valid_read_string(*ext); @ ensures *ext == \null || valid_read_string(*ext); @ assigns *ext; @*/

  @ assigns *ext;
  @*/
static void OLE_parse_uni_software_entry(const char *buffer, const unsigned int size, const unsigned int offset, const char **ext)
{
  if(offset >= size - 8)
  {
    /*@ assert *ext == \null || valid_read_string(*ext); */
    return ;
  }
  /*@ assert offset < size - 8; */
  {
    const unsigned int offset_soft=offset + 8;
    /*@ assert offset_soft < size; */
    const unsigned int count=get32u(buffer, offset + 4);
    unsigned int count2;
    if(count == 0 || count > size/2)
    {
      /*@ assert *ext == \null || valid_read_string(*ext); */
      return ;
    }
    /*@ assert 0 < count <= size/2; */
    count2=2*count;
    /*@ assert 0 < count2 <= size; */
    if(count2 > size - offset_soft)
    {
      /*@ assert *ext == \null || valid_read_string(*ext); */
      return ;
    }
    /*@ assert count2 <= size - offset_soft; */
    /*@ assert offset_soft + count2 <= size; */
    /*@ assert \valid_read(buffer + (0 .. size - 1)) && \initialized(buffer + (0 .. size - 1)); */
    /*@ assert \valid_read(buffer + (0 .. offset_soft + count2 - 1)); */
#ifdef DEBUG_OLE
    {
      unsigned int j;
      log_info("Software ");
      for(j=0; j < count2; j+=2)
      {
	/*@ assert 0 <= j < count2; */
	/*@ assert offset_soft + count2 <= size; */
	const unsigned int tmp=offset_soft + j;
	/*@ assert tmp < size; */
	log_info("%c", buffer[tmp]);
      }
      log_info("\n");
    }
#endif
    *ext=software_uni2ext(&buffer[offset_soft], count);
  }
  /*@ assert *ext == \null || valid_read_string(*ext); */
}

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