Coq VST内部结构复制 [英] Coq VST Internal structure copying

问题描述

针对Coq 8.10.1的VST(已验证软件工具链)2.5v库遇到问题:

run into a problem with VST(Verified Software Toolchain) 2.5v library for Coq 8.10.1:

使用VST的最新工作提交时出错，即"不支持内部结构复制".最小的例子:

Got an error with the latest working commit of VST namely "Internal structure copying is not supported". Minimal example:

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

在启动证明时出现错误:

On starting proof got an error:

错误:策略失败:(_q)％expr表达式包含内部结构复制，这是可验证C(级别97)当前不支持的C功能.

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)存在哪些建议的解决方法?

1) What suggested workarounds exists?

2)出现此限制的原因是什么?

2) What is the reason for this limitation?

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

3) Where can I get a list of unsupported features?

推荐答案

1)解决方法是将C程序更改为逐字段复制.

1) The workaround is to change your C program to copy field by field.

2)原因是C的结构复制异常复杂且依赖于目标ISA的实现/语义，尤其是在参数传递和函数返回中.

2) The reason is the absurdly complicated and target-ISA-dependent implementation/semantics of C's structure-copying, especially in parameter passing and function-return.

3)参考手册列出了一小部分不受支持的功能，但不幸的是，按拷贝复制结构不在该列表中.那是一个错误.

3) The first 10 lines of Chapter 4 ("Verifiable C and clightgen") of the reference manual has a short list of unsupported features, but unfortunately struct-by-copy is not on that list. That's a bug.

这篇关于Coq VST内部结构复制的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！