CompCertSSA
CompCertSSA est une version étendue du compilateur C vérifié CompCert, avec un middle-end SSA pour la construction de la forme SSA, des optimisations SSA-based et des librairies associées. Il prend en charge un sous-ensemble important du langage C et génère du code assembleur pour PowerPC, ARM, x86 et RISC-V.
Cas d'utilisation métiers
- Génération de code assembleur conforme aux spécifications du code C : rechercher des initiatives proches
- Optimisation du code C via une forme SSA intermédiaire : rechercher des initiatives proches
- Compilation de code C sécurisée et vérifiée : rechercher des initiatives proches
- Preuve formelle de la correction du compilateur : rechercher des initiatives proches
Organisation
- Institut national de recherche en informatique et en automatique (organisation rattachée)
Description générée le mercredi 20 mars 2024 à 07:59:01