CompCert's main theorem is that the compiled code maintains or improves the behavior of the source code, as in, it can only maintain or remove erroneous behavio

CompCert's main theorem is that the compiled code maintains or improves the behavior of the source code, as in, it can only maintain or remove erroneous behaviors. So, it can remove a division by zero, for instance, but it will never add one. Otherwise, the compiler does not guarantee the absence of UB; for that, you need Verasco (http://compcert.inria.fr/verasco/ http://compcert.inria.fr/verasco/), a static analyzer that tries to prove that a given code is UB-free. If it succeeds, then combined with CompCert's semantic guarantee, you get a compiled code that is as UB-free as the source code. Verasco was a research project and it's not clear it's still being developed.