1 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
2 <link rel="stylesheet" href="style.css" type="text/css"/>
3 <script src="code.js" type="text/javascript"></script>
5 <h1>nbdkit tvdiff_usec</h1>
8 <a href="https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html">https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html</a>
13 predicate valid_timeval (struct timeval tv) =
14 tv.tv_sec >= 0 && tv.tv_usec >= 0 && tv.tv_usec < 1000000;
15 logic integer tv_to_microseconds (struct timeval tv) =
16 tv.tv_sec * 1000000 + tv.tv_usec;
24 assumes INT64_MIN <= a + b <= INT64_MAX;
26 ensures \result == \false;
28 assumes !(INT64_MIN <= a + b <= INT64_MAX);
29 ensures \result == \true;
31 extern bool __builtin_add_overflow (int64_t a, int64_t b, int64_t *r);
35 assumes INT64_MIN <= a - b <= INT64_MAX;
37 ensures \result == \false;
39 assumes !(INT64_MIN <= a - b <= INT64_MAX);
40 ensures \result == \true;
42 extern bool __builtin_sub_overflow (int64_t a, int64_t b, int64_t *r);
46 assumes INT64_MIN <= a * b <= INT64_MAX;
48 ensures \result == \false;
50 assumes !(INT64_MIN <= a * b <= INT64_MAX);
51 ensures \result == \true;
53 extern bool __builtin_mul_overflow (int64_t a, int64_t b, int64_t *r);
57 /* Return the number of µs (microseconds) *r = *y - *x.
58 * On overflow, returns -1.
61 requires \valid_read (x) && \valid_read (y);
62 requires valid_timeval (*x) && valid_timeval (*y);
66 assumes INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x)
69 ensures *r == tv_to_microseconds (*y) - tv_to_microseconds (*x);
71 assumes !(INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x)
73 ensures \result == -1;
79 tvdiff_usec (const struct timeval *x, const struct timeval *y,
84 if (__builtin_sub_overflow (y->tv_sec, x->tv_sec, &usec)) {
89 if (__builtin_mul_overflow (usec, 1000000, &usec))
91 if (__builtin_add_overflow (usec, y->tv_usec - x->tv_usec, &usec))