c - Verifiable-C 支持 C 的哪个子集？

Question

我试图弄清楚Verified Software Toolchain中的 Verifiable C 支持 C 的哪个子集。“认证编译器的程序逻辑”（第 143 页）声明它是Clight的子集。但是CompCert 编译器将程序从 CompCert C 转换为 Clight。这是否意味着可以通过 Verifiable C 来验证任何 CompCert C 程序？

Answer 1

可验证的 C手册（请参阅第 9 页）指出该仪器可使用 C 的子集，但有一些限制。但是CompCert 安装附带的clightgen工具将 C 翻译成 CompCert 的 Clight 中间语言，因此 Verifiable C 可以使用的子集几乎是整个 C。

Answer 2

事实上，使用 Verifiable C 时，首先使用 CompCert 的解析器/类型检查器将 C 转换为 Clight，因此它实际上并不是关于“C 中有什么但 Clight 中没有”，而是关于“不支持 C 的哪些特性”。参考手册的第 9 页基本上说：

• Verifiable C 不支持 Goto（但 CompCert 支持 goto）。
• Verifiable C 不支持结构复制（通过结构赋值、结构参数）（但我认为 CompCert 支持）
• 只有结构化的 switch 语句（在 VC 或 CompCert 中没有 Duff 的设备）
• 不能将指针转换为整数然后对结果进行算术运算。

这些是主要的限制。