Les compilateurs peuvent dégrader certaines garanties en apportant des optimisations sur l’exécutable. CompCert d’AbsInt apporte ces garanties de compilation de code C tout en optimisant les performances d’exécution. Indispensable pour la validation, la vérification et la certification de logiciels embarqués critiques qui doivent satisfaire aux exigences de sureté de fonctionnement et de cybersécurité tels que les DO178B/C, ISO 26262, IEC 61508, EN 50128 ou ISO 21434.

CompCert est un compilateur C optimisant vérifié formellement. Il est destiné à la compilation de logiciels mission-critiques et pour la sécurité, écrits en C et répondant à des niveaux d’assurance qualité élevés. Il accepte la plupart du langage C 99 de l’ISO, avec quelques exceptions et quelques extensions. Il produit du code machine pour les architectures PowerPC, x86, ARM, AArch64 et RISC-V.
Il est le seul compilateur de production vérifié formellement et garanti exempt de problèmes de compilation. Il est prouvé que le code qu’il produit se comporte exactement comme spécifié par la sémantique du programme C source.

Il implémente les optimisations suivantes, toutes formellement vérifiées: allocation de registres à l’aide de la coloration de graphes et de la coalescence itérative des registres, sélection des instructions avec réduction de la force, pour tirer parti des instructions combinées fournies par les architectures cibles, propagation des constantes pour les types entiers et à virgule flottante, élimination des sous-expressions communes, élimination du code mort, inlining des fonctions, élimination des appels de queue.

Large gamme de processeurs supportés tels les PowerPC (32 bits et hybride 32/64 bits), IA32 (x86 32 bits), AMD64 (x86 64 bits), ARM et AArch64, et RISC-V (32 et 64 bits).

Un outil optionnel appelé Valex est disponible pour la validation postpass des étapes d’assemblage et de liaison. Il compare les instructions du code assembleur abstrait produit par CompCert aux instructions de l’exécutable binaire lié, vérifie si les symboles sont utilisés de manière cohérente, si la taille des variables et les données d’initialisation correspondent, et si les variables sont placées dans les sections appropriées de l’exécutable.

Contactez nous pour une démonstration en ligne ou pour accéder à la version d’évaluation gratuite, avec support technique et formation en ligne.