CompCert akzeptiert ganz ISO C 99 mit den folgenden Ausnahmen:
- Felder von variabler Größe werden nicht unterstützt.
longjmpundsetjmpfunktionieren nicht unbedingt.- Voreingestellt ist, daß
switch-Anweisungen strukturiert sein müssen (wie in MISRA-C). Unterstützung für unstrukturierte Switches (wie in Duff’s Device) kann mithilfe der Kommandozeilenoption-funstructured-switchaktiviert werden.
Insgesamt unterstützt CompCert damit die Teilmenge von C, die MISRA-C 2004 entspricht, sowie viele Features, die von MISRA ausgeschlossen werden (z. B. rekursive Funktionen und dynamische Haldenspeicherallokation).
Darüberhinaus unterstützt CompCert diverse ISO-C-2011-Features:
- Den
_Alignof-Operator und das_Alignas-Attribut. - Anonyme Strukturen und Vereinigungen.
_Static_assert-Anweisungen und_Generic-Ausdrücke.- Unicode-Literale und -Konstanten.
Zusätzlich unterstützt CompCert einige Erweiterungen des ISO C, die vom GNU- bzw. Diab-Compiler übernommen wurden:
- Pragmas und Attribute zur Steuerung der Speicherausrichtung und der Plazierung von globalen Variablen.
- Attribute zur Steuerung von Structure-Packing, Inline-Ersetzung, udgl.
- Eingebaute Funktionen für den Zugriff auf bestimmte prozessorspezifische Instruktionen.
- Inline-Assembler im GNU-Stil.
Jetzt ausprobieren
Testen Sie CompCert kostenlos an Ihren eigenen Anwendungen.