Verifiable-C 支持 C 的哪个子集？
What subset of C is supported by Verifiable-C?
我试图弄清楚来自 Verified Software Toolchain. "Program Logics For Certified Compilers" (p. 143) states that it is subset of Clight. But CompCert compiler 的可验证 C 支持的 C 的哪个子集将程序从 CompCert C 转换为 Clight。这是否意味着可以通过 Verifiable C 验证任何 CompCert C 程序？
可验证的 C manual（请参阅第 9 页）声明该工具使用 C 的子集并具有数量限制。但是CompCert安装附带的clightgen工具将C翻译成CompCert的Clight中间语言，所以Verifiable C可以工作的子集几乎是整个C。
确实，使用 Verifiable C 的人首先使用 CompCert 的 parser/typechecker 将 C 转换为 Clight，因此它并不是真正关于“C 中有什么但 Clight 中没有”，它实际上是关于“C 的哪些功能是不支持。” reference manual 的第 9 页基本上说：
- Verifiable C 不支持 Goto（但 CompCert 支持 goto）。
- 可验证 C 不支持结构复制（通过结构分配、结构参数）（但我认为它在 CompCert 中受支持）
- 只有结构化的 switch 语句（VC 或 CompCert 中没有 Duff 的设备）
- 不能将指针转换为整数然后对结果进行算术运算。
这些是主要的限制。
我试图弄清楚来自 Verified Software Toolchain. "Program Logics For Certified Compilers" (p. 143) states that it is subset of Clight. But CompCert compiler 的可验证 C 支持的 C 的哪个子集将程序从 CompCert C 转换为 Clight。这是否意味着可以通过 Verifiable C 验证任何 CompCert C 程序？
可验证的 C manual（请参阅第 9 页）声明该工具使用 C 的子集并具有数量限制。但是CompCert安装附带的clightgen工具将C翻译成CompCert的Clight中间语言，所以Verifiable C可以工作的子集几乎是整个C。
确实，使用 Verifiable C 的人首先使用 CompCert 的 parser/typechecker 将 C 转换为 Clight，因此它并不是真正关于“C 中有什么但 Clight 中没有”，它实际上是关于“C 的哪些功能是不支持。” reference manual 的第 9 页基本上说：
- Verifiable C 不支持 Goto（但 CompCert 支持 goto）。
- 可验证 C 不支持结构复制（通过结构分配、结构参数）（但我认为它在 CompCert 中受支持）
- 只有结构化的 switch 语句（VC 或 CompCert 中没有 Duff 的设备）
- 不能将指针转换为整数然后对结果进行算术运算。
这些是主要的限制。