时间戳

首页 > 解决方案 > Coq VST 内部结构复制

c - Coq VST 内部结构复制

问题描述

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.vcheck_normalized中的：

Fixpoint check_norm_expr (e: expr) : diagnose_expr :=
match e with
| Evar _ ty => diagnose_this_expr (access_mode ty) e
...

所以，问题是：

1) 存在哪些建议的解决方法？

2) 这种限制的原因是什么？

3) 我在哪里可以获得不受支持的功能列表？

标签： ccoqformal-verificationverifiable-c

解决方案

1）解决方法是将您的C程序更改为逐字段复制。

2）原因是C的结构复制的荒谬复杂和依赖于目标ISA的实现/语义，特别是在参数传递和函数返回中。

3)参考手册第 4 章（“可验证的 C 和 clightgen”）的前 10 行有一个不支持的特性的简短列表，但不幸的是 struct-by-copy 不在该列表中。那是一个错误。

推荐阅读