Function _date_get_seconds

src/common.c:328–331

@ @ requires 0 <= seconds2 <= 31; @ terminates \true; @ ensures 0 <= \result <= 62; @ assigns \nothing; @*/

  @ assigns \nothing;
  @*/
static unsigned long int _date_get_seconds(const unsigned long int seconds2)
{
  return seconds2 << 1;
}

/*@
  @ requires 0 <= m <= 0x3f;