|
|
|
|
|
|
by raphlinus
341 days ago
|
|
|
Yes. The problem here is the -x operation. If INT_MIN is in the array, then the negation operation itself is UB. As you say, the fix is to skip values equal to INT_MIN; it's not possible that its negation is in the array, as that number is not representable. Rust is only a little better. With default settings, it will panic if isize::MIN is in the input slice in a debug build, and in a release build will incorrectly return true if there are two such values in the input. But in C you'll get unicorns and rainbows. |
|
|
But in formally verified C you’ll have the algorithm that’s correct for that type (skip INT_MIN), or you won’t have a proof.