I've always liked the idea of djb's boringcc[0], except with different definitions of undefined based on what users were using C currently with. This would allow people to "upgrade" into boringcc with their current code bases. So with a single invocation of a compiler, you couldn't use more than one set of defined undefined behaviors.
I would love a gcc optimization level, like -Og which only applies optimizations that don't interfere with debugging information, where all undefined behavior is specified.
Does anyone know if undefined behavior is specified in CompCert? Or does CompCert simply not allow you to write programs with undefined behavior?
[0]: https://groups.google.com/forum/m/#!msg/boring-crypto/48qa1k...