Function _date_get_days

src/common.c:318–321

@ @ requires 0 <= days <= 334; @ requires 0 <= year <= 127; @ requires 0 <= leap_day <= 32; @ requires 0 <= day <= 30; @ terminates \true; @ ensures 0 <= \result <= 334 + 127 * 365 + 32 + 30 + DAYS_DELTA; @ assigns \nothing; @*/

  @ assigns \nothing;
  @*/
static unsigned long int _date_get_days(const unsigned long int days, const unsigned long int year, const unsigned long int leap_day, const unsigned long int day)
{
  return days + year * 365 + leap_day + day + DAYS_DELTA;
}
/*@
  @ requires 0 <= seconds2 <= 31;
  @ terminates \true;