Coq VST内部结构复制

Question

Coq 8.10.1的VST(验证软件工具链) 2.5v库遇到了问题：

在VST的最新工作提交中出现了一个错误，即“不支持内部结构复制”。最起码的例子：

struct foo {unsigned int a;};
struct foo f() {
struct foo q;
return q; }

开始时证明出了一个错误：

错误:战术失败:表达式(_q)%expr包含内部结构复制，这是当前可验证的C(97级)中不支持的C特性。

这是由于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)在哪里可以得到不受支持的特性列表？

Answer 1

1)解决办法是将C程序更改为逐个字段复制。

2) C结构复制的复杂性和目标依赖于ISA的实现/语义，特别是在参数传递和函数返回方面。

3) 参考手册第4章的前10行(“可验证的C和clightgen")有一个简短的不受支持的特性列表，但不幸的是，该列表中没有按副本构造的特性。那是个虫子。