En effet, Astrée prouve l'absence d'erreurs d'exécution sur du code C, en utilisant donc le standard du C (je sais pas quelle spec). Si le compilateur C ne respecte pas la norme, effectivement la preuve n'en est pas vraiment une

Mais j'imagine qu'ils font aussi attention à leurs compilos (et à leurs processeurs aussi bien sûr, pasque si le proc respecte pas la norme IEEE sur le calcul des flottants à la lettre, par exemple, ben les preuves d'Astrée ne sont plus valide non plus en cas d'erreur d'arrondi ...).