Function date_dos2unix

src/common.c:362–394

@ @ requires -14*3600 <= secwest <= 12*3600; @ requires f_time <= 0xffffffff; @ requires f_date <= 0xffffffff; @ terminates \true; @ assigns \nothing; @*/

  @ assigns \nothing;
  @*/
time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
{
  static const unsigned int days_in_year[] = { 0, 0,31,59,90,120,151,181,212,243,273,304,334,0,0,0 };
  /* JanFebMarApr May Jun Jul Aug Sep Oct Nov Dec */

  unsigned long int day,leap_day,month,year,days;
  unsigned long int secs;
  year  = f_date >> 9;
  /*@ assert 0 <= year <= 127; */
  month = td_max(1, (f_date >> 5) & 0xf);
  /*@ assert 1 <= month <= 15; */
   day   = td_max(1, f_date & 0x1f) - 1;
  /*@ assert 0 <= day <= 30; */
  leap_day = _date_get_leap_day(year, month);
  /*@ assert 0 <= leap_day <= 32; */
  days = days_in_year[month];
  /*@ assert 0 <= days <= 334; */
  days = _date_get_days(days, year, leap_day, day);
  /*@ assert 0 <= days <= 334 + 127 * 365 + 32 + 30 + DAYS_DELTA; */
  secs = _date_get_seconds(f_time &0x1f);
  /*@ assert secs <= 62; */
  secs += _date_min_to_seconds((f_time >> 5) & 0x3f);
  /*@ assert secs <= 0x3f * SECS_PER_MIN + 62; */
  secs += _date_hours_to_seconds(f_time >> 11);
  /*@ assert secs <= 0x3f * SECS_PER_HOUR + 0x3f * SECS_PER_MIN + 62; */
  secs += days * SECS_PER_DAY;
  /*@ assert secs <= (334 + 127 * 365 + 32 + 30 + DAYS_DELTA)* SECS_PER_DAY + 0x3f * SECS_PER_HOUR + 0x3f * SECS_PER_MIN + 62; */
#if defined(__FRAMAC__)
  return secs;
#else
  return secs+secwest;
#endif
}

void set_secwest(void)
{