X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=2020-frama-c%2F5400-timeval.html;h=c9ee4436809bce943f27851bbdec0bc252329383;hb=3840500fcef75d64b1c23f5c56a340435ac79c59;hp=296d28135302fddba596d550b37f9dfbf9989ded;hpb=b418766b4d897080ff67a6bd3bb558b14ec985d4;p=libguestfs-talks.git diff --git a/2020-frama-c/5400-timeval.html b/2020-frama-c/5400-timeval.html index 296d281..c9ee443 100644 --- a/2020-frama-c/5400-timeval.html +++ b/2020-frama-c/5400-timeval.html @@ -4,27 +4,94 @@
+https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html +
+- /*@ - 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) - ... +/*@ + 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; +}