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)
...