CompCert
CompCert 3.14
Der formell verifizierte C-Compiler.
Der CompcERT C-verifizierte Compiler ist ein Compiler für eine große Teilmenge der C-Programmiersprache, die Code für die Prozessoren PowerPC-, ARM-, X86- und RISC-V-Prozessoren generiert.
Das Unterscheidungsmerkmal von CompCert ist, dass es mit dem CoQ -Proof -Assistenten formell überprüft wurde: Der generierte Assemblercode wird offiziell garantiert, wie sie durch die Semantik des Quell -C -Codes vorgeschrieben ist.
Weitere Informationen zu CompCert (unterstützte Plattformen, unterstützte C -Funktionen, Installationsanweisungen, Verwenden des Compilers usw.) finden Sie auf der Website und insbesondere des Benutzerhandbuchs.
CompCert ist keine kostenlose Software. Diese nichtkommerzielle Veröffentlichung kann nur für die Bewertung, Forschung, Bildung und persönliche Zwecke verwendet werden. Eine kommerzielle Version von Compcert ohne diese Einschränkung sowie mit professionellen Unterstützung und zusätzlichen Funktionen kann von Absint gekauft werden. Weitere Informationen finden Sie in der LICENSE .
Der CompcERT -Verifizierte Compiler ist das Copyright Institut National de Recherde en informatique et en Automatique (INRIA) und Absint Angewandte Informatik GmbH.
Allgemeine Diskussionen über Compcert finden auf der Mailingliste [email protected].
Für Anfragen zur kommerziellen Version von CompCert wenden Sie sich bitte an [email protected]
