That's such a good example for teaching purposes, because it manages to combine the lack of understanding surrounding the remainder operator (i.e. unlike python % in c is not modulus) with the lack of understanding surrounding 0x80000000 (two's complement bane) into a single example. However it still makes my point that in this circumstance, the compiler's strategy still is to do nothing, because it can prove that the check could only be true under undefined behavior circumstances, so doing nothing means not compiling the check. I'm fine with that. Would anyone prefer that the compiler's internal definition of logic assume that absolute values can be negative? Must we throw out centuries of math because we've optimized integers to be 32-bits?

The only thing that's problematic is we need better tools to bring logic assumptions to our attention. Currently, UBSAN can only warn us about that when two's bane actually gets passed to the function at runtime. So the only way to spot faulty logic we failed to consider is to both enable UBSAN and be super methodical about unit testing.

Well, another thing I like to do is just read the assembly output. Constantly. Whenever I write something like a parser I've got a keyboard mapping that shows me the assembly output in Emacs with UBSAN enabled. If I turn off the noisy ones like pointer overflow then I can avoid these issues altogether by writing my code so that no UBSAN assembly gets generated. Since the compiler won't show that as a warning. You literally have to read the -S assembly output to get the compiler warnings that are actually meaningful.

I wish there was an abs() function that returned the unsigned version of the signed input type and wasn't UB if you passed in the most negative value of the signed type. Sadly neither C or C++ nor Rust's standard libraries have a built-in implementation of this, and sending the most negative integer into Rust's .abs() will panic in debug mode (is not intended to be used in properly implemented code).