You can see the statement here: http://compcert.inria.fr/doc/html/Compiler.html#transf_c_program_correct http://compcert.inria.fr/doc/html/Compiler.html#transf_

You can see the statement here: http://compcert.inria.fr/doc/html/Compiler.html#transf_c_program_correct http://compcert.inria.fr/doc/html/Compiler.html#transf_c_pro... A C compiler doesn't have to promise much of anything about the behavior of the code produced for a program with undefined behavior. This statement could be vacuous for a program p with undefined behavior if (Cstrategy.exec_program p beh) isn't true for any behavior beh, or only true for a behavior which makes (not_wrong beh) false. If they don't always, then they actually give you a guarantee for some bad programs as well. Nothing in the spec says running a bad program has to make demons fly out your nose.