什么子集的C是支持可验证-C？

Question

我试图找出验证软件工具链的可验证C支持哪个子集。“认证编译器的程序逻辑”(第143页)指出，它是克莱的子集。但是CompCert编译器将程序从CompCert C转换为Clight。这是否意味着可以通过可验证的C来验证任何CompCert C程序？

Answer 1

实际上，使用可验证的C首先使用CompCert的解析器/打字机将C转换为Clight，所以它实际上不是关于“C中的什么，而不是Clight中的什么”，而是“C的哪些特性不受支持”。参考手册的第9页基本上是这样的：

• 在可验证的C中不支持Goto (但CompCert支持goto)。
• 结构复制(通过结构赋值，结构参数)在可验证的C中不支持(但我认为在CompCert中是支持的)
• 只有结构化开关语句(在VC或CompCert中都没有达夫的设备)
• 不能将指针转换为整数，然后对结果执行算术。

这些是主要的限制。

Answer 2

可验证的C 手册 (见第9页)指出，该仪器与C的子集一起工作，并有数量限制。但是CompCert安装附带的clightgen工具将C转换成CompCert的Clight中间语言，因此可验证的C可以使用的子集几乎是整个C。