Displaying 1 result from an estimated 1 matches for "__builtin_sub_overflow".
Did you mean:
__builtin_mul_overflow
2020 Oct 17
0
[PATCH nbdkit] common/include/tvdiff.h: Add formal specification.
..., 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 == \tr...