Nitpicking, the test itself should avoid overflowing. Instead, test "a <= UINT_MAX - b" to prove no overflow occurs.

For signed integers, we need to prove the following without overflowing in the test: "a+b <= INT_MAX && a+b >= INT_MIN". The algorithm follows: test "b >= 0", which implies "INT_MAX-b <= INT_MAX && a+b >= INT_MIN", so then test "a <= INT_MAX-b". Otherwise, "b < 0", which implies "INT_MIN-b >= INT_MIN && a+b <= INT_MAX", so then test "a >= INT_MIN-b".