3 ms·

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://compc

by dhekir 9y ago

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 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.

tom_mellior 9y ago
CompCert doesn't verify C, it compiles it. And like any compiler, it uses the type sizes defined by the ABI it targets.
MaxBarraclough 9y ago
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.

by dhekir 9y ago

tom_mellior 9y ago

CompCert doesn't verify C, it compiles it. And like any compiler, it uses the type sizes defined by the ABI it targets.

MaxBarraclough 9y ago

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.