CompCert

compcert

正式验证的C编译器。

概述

CompCert C验证的编译器是C编程语言的大量子集的编译器，可为PowerPC，ARM，X86和RISC-V处理器生成代码。

CompCert的区别特征是它已使用COQ证明助手进行了正式验证：生成的汇编代码可以正式保证按照源C代码的语义规定的规定。

有关COMPCERT（支持的平台，支持的C功能，安装说明，使用编译器等）的更多信息，请参阅网站，尤其是用户手册。

执照

CompCert不是免费软件。此非商业版本只能用于评估，研究，教育和个人目的。可以从ABSINT购买商业版的CompCert，没有这种限制，没有专业支持和额外功能。有关更多信息，请参见文件LICENSE 。

版权

经过验证的编译器是版权所有Informatique et Automatique（Inria）和Absint Angewandte Informatik GmbH。

接触

关于CompCert的一般讨论在[email protected]邮件列表上进行。

有关Compcert商业版本的查询，请联系[email protected]