Sure, but this does not seem to provide any insight into how, in this compiler, the preservation of semantics under optimization plays out in optimizations which assume the program will never attempt to perform UB.
"The semantics of undefined behaviour are exactly the same before and after any transformation of the program"
[emphasis added]
I think you've got this idea that Undefined Behaviour somehow means that the behaviour is defined but is being kept secret from you. It isn't. The behaviour really is Undefined. Doing further transformations to it is therefore always harmless.
I don’t think you are getting that Undefined is a concept in the language specification domain, that is not literally implemented. Consequently, you don’t even see yet what my question is about. When I think of a way to make it clearer, I will follow up.
The C standard Appendix J.2 contains an incomplete list of undefined behavior causes. Note that some of them simply cannot be checked at compile time, eg "The execution of a program contains a data race (5.1.2.4)" cannot have the semantics of the resulting program defined by the compiler. C does not provide the compiler with enough information to statically prevent data races. I'm not familiar with CompCert, but it should be possible to go through appendix J.2 and find the UB causes which are detectable at compile time, and then go through CompCert and see what it does for each. What it does will likely depend on the particular program it's compiling, of course.