Les nombres flottants tels que définis dans le standard IEEE-754 sont la solution la plus répandue pour approximer les nombres réels en machine. Toutefois, en pratique, de nombreux environnements logiciels et matériels présentent des subtilités non conformes avec ce standard. Cela complique la tâche de raisonner formellement sur les programmes effectuant des calculs numériques sans connaître a priori leur environnement d'exécution. Dans cet article, nous montrons l'impact de ce problème sur le compilateur CompCert, un compilateur formellement vérifié pour le langage C et proposant un support pour les flottants IEEE-754. Nous présentons les résultats d'un travail d'investigation visant à mesurer les difficultés liées à l'intégration de nouveaux types de flottants dans CompCert. Cette étude est motivée par la volonté d'étendre le compilateur à des cibles non conformes IEEE-754 utilisées, par exemple, en informatique embarquée.