Displaying 1 result from an estimated 1 matches for "valid_timeval".
2020 Oct 17
0
[PATCH nbdkit] common/include/tvdiff.h: Add formal specification.
...@@ -37,28 +37,134 @@
#include <config.h>
+#include <stdbool.h>
+#include <stdint.h>
#include <sys/time.h>
-/* 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...