  CompCert is the first realistic formally verified compiler: it provides a
machine-checked mathematical proof that the code it generates matches the
source code. Yet, there could be loopholes in this approach. We comprehensively
analyze aspects of CompCert where errors could lead to incorrect code being
generated. Possible issues range from the modeling of the source and the target
languages to some techniques used to call external algorithms from within the
compiler.
