That's a good example. I see two ways to handle that one:
1. Don't use int, use a type that gives stronger range assurances, like int_fast32_t (though I'm not sure at a glance what's the minimum legal value of INT_FAST32_MAX)
2. Put a compile-time assert to ensure that your range assumptions are met by the target platform's 'int'
A pity that Ada's 'range types' approach to fixed-point types never caught on. It solves this platform-variance question, expresses the programmer's intent better, and enables useful runtime checks. It's possible with C++ templates (libraries exist for the purpose), but no-one does it.
As for the question of what our static/dynamic analysis tools should do: they should be paranoid, and warn that the code might invoke UB, unless specifically configured to make strong platform assumptions. By default, we should aim to write good portable C.
Even CompCert, the formally verified C compiler, had to make some concessions concerning the standard: it does not verify C per se, but CompCert C (http://compcert.inria.fr/man/manual005.html), which is very close to C99 but with fixed-size integers (32-bit), two's complement signed integers (so no UB in signed overflows), etc.
Otherwise, it is practically impossible to find some actually useful C code that is fully portable and compliant.
But I agree that analysis tools should be as configurable as possible, and report UB whenever they can. However, if the default settings lead to way too many false positives, the users might end up giving up before learning how to turn some of them off. It's a delicate balance between paranoia and usability. Even -Wall -Wextra -pedantic do not activate all warnings about detectable UBs, and that's about as paranoid as you can get in GCC/Clang.
As tom_mellior says, CompCert is just a compiler, and it's not deviating from the C standard.
The C standard says that sizeof(int) is implementation defined. CompCert has to choose a size, and they go with the unsurprising choice of 32-bit.
As for no UB in signed overflows: where the C standard says 'undefined behavior', that doesn't prohibit an implementation (i.e. a compiler) from picking a well-defined behavior. It just means that portable code mustn't rely on that behavior - build such code on a different standards-compliant compiler and you might end up with demons flying out of your nose, etc.
> it is practically impossible to find some actually useful C code that is fully portable and compliant.
Disagree. The C/C++ code I've written has been portable and standard. The hardest part was that CMake is a trainwreck.
> if the default settings lead to way too many false positives, the users might end up giving up before learning how to turn some of them off
That's more an issue with legacy code that when writing new code.
1. Don't use int, use a type that gives stronger range assurances, like int_fast32_t (though I'm not sure at a glance what's the minimum legal value of INT_FAST32_MAX)
2. Put a compile-time assert to ensure that your range assumptions are met by the target platform's 'int'
A pity that Ada's 'range types' approach to fixed-point types never caught on. It solves this platform-variance question, expresses the programmer's intent better, and enables useful runtime checks. It's possible with C++ templates (libraries exist for the purpose), but no-one does it.
As for the question of what our static/dynamic analysis tools should do: they should be paranoid, and warn that the code might invoke UB, unless specifically configured to make strong platform assumptions. By default, we should aim to write good portable C.