--- /dev/null
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<link rel="stylesheet" href="style.css" type="text/css"/>
+<script src="code.js" type="text/javascript"></script>
+
+<h1>nbdkit tvdiff_usec</h1>
+
+<pre class="code">
+ /*@
+ 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)
+ ...
+</pre>