I believe Compcert still translates programs with undefined behavior and doesn't really do anything about it; or rather, the behavior is defined but based on whatever the Compcert authors define the behavior to be.