Function _date_min_to_seconds

src/common.c:339–342

@ @ requires 0 <= m <= 0x3f; @ terminates \true; @ ensures 0 <= \result <= 0x3f * SECS_PER_MIN; @ assigns \nothing; @*/

  @ assigns \nothing;
  @*/
static unsigned long int _date_min_to_seconds(const unsigned long int m)
{
  return m * SECS_PER_MIN;
}

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