问题标签 [verifiable-c]

Coq 8.10.1 的 VST（已验证软件工具链）2.5v 库遇到问题：

VST 的最新工作提交出现错误，即“不支持内部结构复制”。最小的例子：

在开始证明时出现错误：

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

这是由于floyd/forward.vcheck_normalized中的：

所以，问题是：

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

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

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

我正在使用 VST 2.5 和 Coq 8.11.0

forward_call使用非标准调用约定执行函数时出错。最小代码示例：

VST 规格：

错误：

我不知道这是错误还是预期行为，所以我在这里有几个问题：

1）这是一个错误吗？

2）如果不是，有什么解决方法可以证明这种情况？

更新：

在使用以下解决结构复制限制的解决方法后，我们遇到了这个问题：我们struct_normalize : statement -> statement在 Coq 中定义了一个函数，用逐字段赋值替换结构赋值。因此，我们假设我们正在调用的函数中没有结构复制。也就是说，我们可以test_aux从上面的例子中验证。所以问题是：

3. forward_call失败只是因为cc_structret := true在test_auxAST中吗？

4. 鉴于我们对函数进行规范化并从函数体中删除结构复制，相应地更改structret值并继续证明是否安全？

我有一个问题，关于 VST 对 compcert 内置注释机制的支持。假设我们有一个C函数：

及其规格：

当我试图证明这一点时，我到达了我有这个声明的状态(builtin EF_annot 1 "_p <> nullval" []([]);

证明下一个，我不能从这里继续前进。

hint策略没有帮助，forward它的变体（如果，循环等）也不起作用。

所以问题是，我如何（如果可以的话）从这里继续前进？

C ISO 99 标准支持所谓的“类型双关”。这是一个小例子：

如您所见，这里我们使用联合类型const通过访问具有相同类型但没有const.

VST：

如果您运行此 coq 代码，您将到达无法证明的目标（在评论中提到），VST 会检查我们是否尝试从联合中获取初始化字段。它看起来如下：

False通过entailer!战术转变为。

所以，问题是：1）为什么 VST 将联合表示为不相交的总和？

2) VST 不支持此功能（类型双关语）吗？

3) 除了编辑 C 代码之外，是否有解决此问题的方法？

我正在开发涵盖可验证 C 的 beta 5 软件基础模块。我在最后一部分，这与哈希映射上的操作有关（这需要对链表进行操作）。

https://www.cs.princeton.edu/~appel/vc/vc-0.9.5/Verif_hash.html

我有点坚持body_incr_list。

正在验证的代码：

这做了一些新的事情......一个指针的指针，以及进入循环的 p 为 null 的事实，但如果它循环，则保证有一个值。该模块给出的规范是：

整个练习取决于适当的循环不变量。这是我的尝试

有了这个，我能够取得一些基本进展，但我陷入了以下处理：

原因是现在在 SEP 子句中，我有listboxrep al' r0'，但是为了让它越过这条线

我需要把它展开成data_at Ews (tptr tcell) p r0' * listrep al' p. 同样，这不是一个大问题，但在 p 为 null 并且它创建新单元格 ( *r = new_cell(s,1,NULL); return;) 的情况下，我得到了一个我不知道是否可以解决的证明目标。

这是因为data_at Ews (tptr tcell) p r0'被转换成data_at Ews (tptr tcell) vret r0'，但我们仍然只是有listrep al' p，没有listrep al' vret。虽然在这种情况下，al' 很可能是 []，这意味着我们有listrep [] p，尽管我不确定可以用它做什么。如果我遵循这一点，我最终会得到以下蕴涵：

这让我相信我的不变量是不正确的......例如，如果我进行调整以将 p 设置为

那么它当然需要为nullval。但我们拥有的价值是data_at Ews (tptr tcell) vret r0'......

所以我不知道。我很确定我需要改进我的不变量，但不知道如何！将不胜感激任何指针。

我正在验证使用数组存储异构数据的 ac 程序 - 特别是，该程序使用数组来实现 cons 单元，其中数组的第一个元素是整数值，第二个元素是指向下一个 cons 单元的指针.

例如，此列表的自由操作将是：

注意：此处未显示，但其他代码部分将读取数组的值并将其视为整数。

虽然我知道表达这一点的自然方式是某种结构，但程序本身是使用数组编写的，我无法更改这一点。

我应该如何在 VST 中指定内存的结构？

我定义了一个lseg谓词如下：

但是，我在尝试评估时遇到了麻烦，void *n = *(void **)x;大概是因为规范声明内存包含整数数组而不是指针。

我有一个关于使用 VST 和 switch 语句的问题。

当 switch 变量存在匹配的情况时，我无法编写逐步执行 switch 语句的证明。例如：

我可以为这样的事情写一个证明：

但是我不能为这样的事情写证明：

每当有“x”的匹配案例（如我的第二个代码示例）时，我在尝试为 switch 语句编写策略时遇到“没有匹配的匹配子句”错误。

通常我可以写类似：“forward_if”、“forward_if True”、“forward_if (PROP() LOCAL() SEP())”，它们适用于我的第一个代码示例，但不适用于我的第二个代码示例。

总而言之：第二个代码示例的证明中的下一行应该是什么？

提前致谢！

由于各种原因，我正在验证一个尝试从偏移量为 0 的指针读取的程序：

在 VST 中验证这一点时，上下文假设在此位置的堆上有一个值：

但是，当尝试forward遍历读取时，证明卡住了错误：

但是如果我将前提条件调整为

或更改源代码，以便改为：

有没有办法在不改变源代码或程序规范的情况下验证这个程序？我怎样才能让阅读通过？

我试图弄清楚Verified Software Toolchain中的 Verifiable C 支持 C 的哪个子集。“认证编译器的程序逻辑”（第 143 页）声明它是Clight的子集。但是CompCert 编译器将程序从 CompCert C 转换为 Clight。这是否意味着可以通过 Verifiable C 来验证任何 CompCert C 程序？

我正在阅读软件基础第 5 册。

在通过 body_push_increasing (verif-triang) 工作时，我试图通过调用来推送。之前的上下文是：

我正在尝试的命令是

消息失败

推送的规范是

（C 表示typedef struct cons *stack;堆栈没有单元素结构）

我究竟做错了什么？