Function _date_hours_to_seconds

src/common.c:350–353

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

  @ assigns \nothing;
  @*/
static unsigned long int _date_hours_to_seconds(const unsigned long int h)
{
  return h * SECS_PER_HOUR;
}

/*@
  @ requires -14*3600 <= secwest <= 12*3600;