nbdkit tvdiff_usec

  /*@
    requires \valid_read (x) && \valid_read (y);
    requires valid_timeval (*x) && valid_timeval (*y);
    requires \valid (r);
    assigns *r;
    behavior success:
      ensures \result == 0;
      ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x);
              INT64_MIN <= diff <= INT64_MAX &&
              *r == diff;
    behavior failure:
      ensures \result == -1;
      ensures *r == 0;
      ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x);
              !(INT64_MIN <= diff <= INT64_MAX);
    complete behaviors;
    disjoint behaviors;
   */
  static inline int
  tvdiff_usec (const struct timeval *x, const struct timeval *y,
               int64_t *r)
  ...