Je ne connais pas bien la sémantique du C mais, pour l'exemple du journal, il me semble bien que l'optimisation de clang ne respecte pas ces principes.
Si l'exemple du journal correspond vraiment à un comportement indéfini, alors le théorème de CompCert ne dit rien à son sujet, a priori :
En traduction, ça veut dire que si le code compilé a un certain comportement, alors un des comportements possibles du source correspond à une « amélioration » de ce comportement (ce qui fait écho à ton commentaire). Par contre, s'il y a un comportement indéfini du source, donc sémantique non définie, je pense pas que ça dise quoi que ce soit d'utile (on obtient juste un comportement « go wrong » accompagné d'une trace dès que la sémantique bloque, donc au mieux ça dirait peut-être que jusqu'au moment où ça bloque la sémantique est préservée).
[^] # Re: Comportement attendu
Posté par anaseto . En réponse au journal Compilateur trop intelligent. Évalué à 2.
Si l'exemple du journal correspond vraiment à un comportement indéfini, alors le théorème de CompCert ne dit rien à son sujet, a priori :
En traduction, ça veut dire que si le code compilé a un certain comportement, alors un des comportements possibles du source correspond à une « amélioration » de ce comportement (ce qui fait écho à ton commentaire). Par contre, s'il y a un comportement indéfini du source, donc sémantique non définie, je pense pas que ça dise quoi que ce soit d'utile (on obtient juste un comportement « go wrong » accompagné d'une trace dès que la sémantique bloque, donc au mieux ça dirait peut-être que jusqu'au moment où ça bloque la sémantique est préservée).