4 ms·
I did not fail to take that into account: > it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was t
by anyfoo 6y ago
I did not fail to take that into account:
> it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x)
And it does not matter, since the point of formal verification is to help taking those issues into account.
- Sharlin 6y agoPardon me if I'm missing something, but I only see the "natural number" case and the "unsigned" case (the latter of which is indeed well-defined to wrap around to zero in C and C++), but I was talking about the case where x and y have, say, type signed int. Then all bets are off if y happens to equal INT_MAX in some execution, because the compiler is allowed to optimize with the assumption that that literally cannot happen. At least as far as the C standard is concerned. So my point was that in the real world, even such a trivial function may not only yield unexpected results but indeed cause the whole program to have arbitrary, undefined behavior.