Function OLE_parse_filetime_entry

src/file_doc.c:1146–1161

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

  @ assigns *file_time;
  @*/
static void OLE_parse_filetime_entry(const char *buffer, const unsigned int size, const unsigned int offset, time_t *file_time)
{
  uint64_t tmp;
  if(offset + 12 > size)
  {
    return ;
  }
  /*@ assert offset + 12 <= size; */
  tmp=get64u(buffer, offset + 4);
  tmp/=10000000;
  if(tmp > (uint64_t)134774 * 24 * 3600)
  {
    tmp -= (uint64_t)134774 * 24 * 3600;
    *file_time=tmp;
  }
}

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