Je veux dire, est-ce qu'il y a eu des initiatives pour faire un compilateur qui donne une sémantique à tous ces comportements indéfinis, quitte à sacrifier un peu en performance, avec crash assuré quand il ne peut pas faire mieux ? Parce que même CompCert (prouvé en Coq) pour C ne donne pas de garanties s'il y a des comportements indéfinis pour lesquels la sémantique bloque (même si le compilo essaie en pratique d'éviter d'être trop intelligent, j'ai l'impression, mais le théorème ne dit rien sur ça).
# Existe-t-il des compilateurs C/C++ qui donnent une sémantique à tous les programmes ?
Posté par anaseto . En réponse au journal Compilateur trop intelligent. Évalué à 2.
Je veux dire, est-ce qu'il y a eu des initiatives pour faire un compilateur qui donne une sémantique à tous ces comportements indéfinis, quitte à sacrifier un peu en performance, avec crash assuré quand il ne peut pas faire mieux ? Parce que même CompCert (prouvé en Coq) pour C ne donne pas de garanties s'il y a des comportements indéfinis pour lesquels la sémantique bloque (même si le compilo essaie en pratique d'éviter d'être trop intelligent, j'ai l'impression, mais le théorème ne dit rien sur ça).