Displaying 1 result from an estimated 1 matches for "tv_to_microsecond".
Did you mean:
tv_to_microseconds
2020 Oct 17
0
[PATCH nbdkit] common/include/tvdiff.h: Add formal specification.
...Return the number of µs (microseconds) in y - x. */
-static inline int64_t
-tvdiff_usec (const struct timeval *x, const struct timeval *y)
+/*@
+ 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...