Eliminating undefined behavior from the language is a language design issue orthogonal to the problem CompCert is trying to solve.