News for hackers. Stuff that matters.
Re:Select Code_execution from * Using SQLite; (2019) by anyfoo on Saturday June 13, 2020 @09:53PM (#23514483)
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.

Re:Select Code_execution from * Using SQLite; (2019) by Sharlin on Sunday June 14, 2020 @02:28PM (#23519995)
Pardon 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.