nbdkit tvdiff_usec

  /*@
    predicate valid_timeval (struct timeval tv) =
      tv.tv_sec >= 0 && tv.tv_usec >= 0 && tv.tv_usec < 1000000;
    logic integer tv_to_microseconds (struct timeval tv) =
      tv.tv_sec * 1000000 + tv.tv_usec;
   */

  /* Return the number of µs (microseconds) in y - x. */
  /*@
    requires \valid_read (x) && \valid_read (y);
    requires valid_timeval (*x) && valid_timeval (*y);
    ensures \result == tv_to_microseconds (*y) - tv_to_microseconds (*x);
   */
  static inline int64_t
  tvdiff_usec (const struct timeval *x, const struct timeval *y)
  {
    int64_t usec;

    usec = (y->tv_sec - x->tv_sec) * 1000000;
    usec += y->tv_usec - x->tv_usec;
    return usec;
  }