nbdkit tvdiff_usec

https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html

/*@
  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;
 */

#ifdef FRAMA_C

/*@
   assigns *r;
   behavior success:
     assumes INT64_MIN <= a + b <= INT64_MAX;
     ensures *r == a + b;
     ensures \result == \false;
   behavior overflow:
     assumes !(INT64_MIN <= a + b <= INT64_MAX);
     ensures \result == \true;
 */
extern bool __builtin_add_overflow (int64_t a, int64_t b, int64_t *r);
/*@
   assigns *r;
   behavior success:
     assumes INT64_MIN <= a - b <= INT64_MAX;
     ensures *r == a - b;
     ensures \result == \false;
   behavior overflow:
     assumes !(INT64_MIN <= a - b <= INT64_MAX);
     ensures \result == \true;
 */
extern bool __builtin_sub_overflow (int64_t a, int64_t b, int64_t *r);
/*@
   assigns *r;
   behavior success:
     assumes INT64_MIN <= a * b <= INT64_MAX;
     ensures *r == a * b;
     ensures \result == \false;
   behavior overflow:
     assumes !(INT64_MIN <= a * b <= INT64_MAX);
     ensures \result == \true;
 */
extern bool __builtin_mul_overflow (int64_t a, int64_t b, int64_t *r);

#endif /* FRAMA_C */

/* Return the number of µs (microseconds) *r = *y - *x.
 * On overflow, returns -1.
 */
/*@
  requires \valid_read (x) && \valid_read (y);
  requires valid_timeval (*x) && valid_timeval (*y);
  requires \valid (r);
  assigns *r;
  behavior success:
    assumes INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x)
                      <= INT64_MAX;
    ensures \result == 0;
    ensures *r == tv_to_microseconds (*y) - tv_to_microseconds (*x);
  behavior failure:
    assumes !(INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x)
                        <= INT64_MAX);
    ensures \result == -1;
    ensures *r == 0;
  complete behaviors;
  disjoint behaviors;
 */
static inline int
tvdiff_usec (const struct timeval *x, const struct timeval *y,
             int64_t *r)
{
  int64_t usec;

  if (__builtin_sub_overflow (y->tv_sec, x->tv_sec, &usec)) {
  overflow:
    *r = 0;
    return -1;
  }
  if (__builtin_mul_overflow (usec, 1000000, &usec))
    goto overflow;
  if (__builtin_add_overflow (usec, y->tv_usec - x->tv_usec, &usec))
    goto overflow;

  *r = usec;
  return 0;
}