Il me semble qu'il n'y a pas si longtemps il avait été question d'un petit bug dans la sémantique de C de CompCert, quelque chose qui avait avoir avec les pointeurs. Je sais, c'est pas très précis, mais je n'y avais pas prêté beaucoup d'attention, donc c'est tout ce que j'ai retenu :)
En tous cas, c'est sûr que la surface où peuvent se trouver des bugs par rapport à un compilateur normal est minime.
[^] # Re: Nuance
Posté par anaseto . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 2.
Il me semble qu'il n'y a pas si longtemps il avait été question d'un petit bug dans la sémantique de C de CompCert, quelque chose qui avait avoir avec les pointeurs. Je sais, c'est pas très précis, mais je n'y avais pas prêté beaucoup d'attention, donc c'est tout ce que j'ai retenu :)
En tous cas, c'est sûr que la surface où peuvent se trouver des bugs par rapport à un compilateur normal est minime.