https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html
/*@ 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 + b <= INT64_MAX); ensures \result == \true; */ extern bool __builtin_add_overflow (int64_t a, int64_t b, int64_t *r); /*@ assigns *r; behavior success: assumes INT64_MIN <= a - b <= INT64_MAX; ensures *r == a - b; ensures \result == \false; behavior overflow: assumes !(INT64_MIN <= a - b <= INT64_MAX); ensures \result == \true; */ extern bool __builtin_sub_overflow (int64_t a, int64_t b, int64_t *r); /*@ assigns *r; behavior success: assumes INT64_MIN <= a * b <= INT64_MAX; ensures *r == a * b; ensures \result == \false; behavior overflow: assumes !(INT64_MIN <= a * b <= INT64_MAX); ensures \result == \true; */ extern bool __builtin_mul_overflow (int64_t a, int64_t b, int64_t *r); #endif /* FRAMA_C */ /* Return the number of µs (microseconds) *r = *y - *x. * On overflow, returns -1. */ /*@ requires \valid_read (x) && \valid_read (y); requires valid_timeval (*x) && valid_timeval (*y); requires \valid (r); assigns *r; behavior success: assumes INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x) <= INT64_MAX; ensures \result == 0; ensures *r == tv_to_microseconds (*y) - tv_to_microseconds (*x); behavior failure: assumes !(INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x) <= INT64_MAX); ensures \result == -1; ensures *r == 0; complete behaviors; disjoint behaviors; */ static inline int tvdiff_usec (const struct timeval *x, const struct timeval *y, int64_t *r) { int64_t usec; if (__builtin_sub_overflow (y->tv_sec, x->tv_sec, &usec)) { overflow: *r = 0; return -1; } if (__builtin_mul_overflow (usec, 1000000, &usec)) goto overflow; if (__builtin_add_overflow (usec, y->tv_usec - x->tv_usec, &usec)) goto overflow; *r = usec; return 0; }