News for hackers. Stuff that matters.
Re:My first verified imperative program by addaon on Monday July 07, 2025 @07:43PM (#44495684)
> If you have INT_MIN along with any other negative number in the array then your program has undefined behavior in C.

What? Why? There’s no addition needed to solve this problem. The example implementation does invert each element, which is undefined for INT_MIN, but it would be trivial to just skip INT_MIN elements (since their additive inverse is never in the set).

Re:My first verified imperative program by raphlinus on Monday July 07, 2025 @08:39PM (#44495915)
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.

Re:My first verified imperative program by addaon on Tuesday July 08, 2025 @12:19AM (#44497047)
> 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.

Re:My first verified imperative program by ykonstant on Tuesday July 08, 2025 @04:03AM (#44498051)
But I like unicorns and rainbows! ...unless my name is Charlie 「(°ヘ°)