Function OLE_parse_software_entry

src/file_doc.c:956–1010

@ @ requires 8 <= size <= 1024*1024; @ requires offset <= 1024*1024; @ 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_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 count=get32u(buffer, offset + 4);
    const unsigned int offset_soft=offset + 8;
    /*@ assert offset_soft == offset + 8; */
    if(count == 0 || count > size)
    {
      /*@ assert *ext == \null || valid_read_string(*ext); */
      return ;
    }
    /*@ assert 0 < count <= size; */
    if(offset_soft + count > size)
    {
      /*@ assert *ext == \null || valid_read_string(*ext); */
      return ;
    }
    /*@ assert offset_soft + count <= size; */
    /*@ assert \valid_read(buffer + (0 .. size-1)); */
    /*@ assert \forall int j; (0 <= j < size ) ==> \valid_read(buffer + j + (0 .. size-1-j)); */
    /*@ assert 0 <= offset_soft < size; */
    /*@ assert \valid_read(buffer + offset_soft + (0 .. size - offset_soft -1)); */
    /*@ assert 0 < count <= size - offset_soft; */
    /*@ assert \valid_read(buffer + offset_soft + (0 .. count -1)); */

    /*@ assert offset_soft + count <= size; */
    /*@ assert count <= size - offset_soft; */
    /*@ assert \valid_read(buffer + (0 .. size-1)); */
    /*@ assert \valid_read(buffer + (0 .. offset_soft + count -1)); */
#ifdef DEBUG_OLE
    {
      unsigned int j;
      log_info("Software ");
      for(j=0; j<count; j++)
      {
	/*@ assert 0 <= j < count; */
	/*@ assert offset_soft + count <= size; */
	const unsigned int tmp=offset_soft+j;
	/*@ assert tmp < size; */
	log_info("%c", buffer[tmp]);
      }
      log_info("\n");
    }
#endif
    software2ext(ext, &buffer[offset_soft], count);
    /*@ assert *ext == \null || valid_read_string(*ext); */
  }
  /*@ assert *ext == \null || valid_read_string(*ext); */
}

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