Coq 8.10.1 的 VST(验证软件工具链)2.5v 库遇到问题:
VST 的最新工作提交出现错误,即“不支持内部结构复制”。 最小示例:
struct foo {unsigned int a;};
struct foo f() {
struct foo q;
return q; }
启动证明时出现错误:
Error: Tactic failure: The expression (_q)%expr contains internal structure-copying, a feature of C not currently supported in Verifiable C (level 97).
这是由于 floyd/forward.v 中的 check_normalized
造成的:
Fixpoint check_norm_expr (e: expr) : diagnose_expr :=
match e with
| Evar _ ty => diagnose_this_expr (access_mode ty) e
...
所以,问题是:
1) 有哪些建议的解决方法?
2) 造成此限制的原因是什么?
3) 从哪里可以获得不支持的功能列表?
最佳答案
1) 解决方法是将 C 程序更改为逐字段复制。
2) 原因是 C 结构复制的极其复杂且依赖于目标 ISA 的实现/语义,尤其是在参数传递和函数返回方面。
3) reference manual 第 4 章(“可验证的 C 和 clightgen”)的前 10 行有一个不支持的功能的简短列表,但不幸的是 struct-by-copy 不在该列表中。这是一个错误。
关于Coq VST 内部结构复制,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/60710135/