This compiler provably follows the semantics allowed (and defined by) the C standard. Optimiaztions have nothing to do with UB. Optimizations simply aim to prod

This compiler provably follows the semantics allowed (and defined by) the C standard. Optimiaztions have nothing to do with UB. Optimizations simply aim to produce more efficient machine code that still matches the semantics as defined by the C standard. Non-optimizing compilers (or this compiler with optimizations off) can (and often do) produce exactly the same output. The C standard Appendix J.2 contains an incomplete list of undefined behavior causes. Note that some of them simply cannot be checked at compile time, eg "The execution of a program contains a data race (5.1.2.4)" cannot have the semantics of the resulting program defined by the compiler. C does not provide the compiler with enough information to statically prevent data races. I'm not familiar with CompCert, but it should be possible to go through appendix J.2 and find the UB causes which are detectable at compile time, and then go through CompCert and see what it does for each. What it does will likely depend on the particular program it's compiling, of course.