CompCert C supports all of ISO C 99, with the following exceptions:
switch statements must be structured as in MISRA-C; unstructured "switch", as in Duff's device, is not supported.
longjmp and setjmp are not guaranteed to work.
Variable-length array types are not supported.
Consequently, CompCert supports all of the MISRA-C 2004 subset of C, plus many features excluded by MISRA (such as recursive functions and dynamic heap memory allocation).
Several extensions to ISO C 99 are supported:
The _Alignof operator and the _Alignas attribute from ISO C2011.
Pragmas and attributes to control alignment and section placement of global variables.
Je pense que cela parlera plus aux développeurs C qu'à moi-même. Et pour l'architecture, on trouve ce schéma :
compcert
De ce que j'ai compris, la certification commence après la traduction en Clight.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Clight
Posté par kantien . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 8.
Je ne sais pas trop, je ne suis que le messager et je ne connais pas les entrailles du système. Sur le site du projet, à la page consacrée à son fonctionnement, on peut y lire :
Je pense que cela parlera plus aux développeurs C qu'à moi-même. Et pour l'architecture, on trouve ce schéma :
compcert
De ce que j'ai compris, la certification commence après la traduction en Clight.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.