问题标签 [verifiable-c]

我目前正在尝试学习如何使用 VST。我正在使用 VST 1.5。我有这个小 C 程序（backref.c）：

我的 Coq 代码（带有微不足道的前置条件和后置条件）是

作为前提，我想说out[-dist]toout[-1]是可读的，out[0]toout[length-1]是可写的。PLCC 第 210 页讲述了一个条件array_at_range，但它似乎在 VST 1.5 中不可用。我怎样才能做到这一点？

更新：现在我有以下程序swap.c：

我的规格是

现在我被卡住了：我可以展开eval_binop，并尝试继续展开，但它并没有真正收敛到我可以使用的任何东西。此外，我不确定如何使用 `eq 属性来实际重写任何内容。

我刚刚开始使用可验证的 c 工作，并且正在努力为我编写的 C 代码生成功能规范。我正在使用的基本示例是（C 代码）

而且我很难将定义 xor_spec 部分放在一起。

谢谢。

VST 版本 1.7。

当我尝试在函数调用中使用它们时，我遇到了一个问题，即 coq 无法识别本地声明的变量。我有代码：

使用 coq 类型位：列表 Z，invKey：Z，大小：Z。

我成功地完成了 bit = bits[i] 步骤，但是当我尝试使用

该步骤失败，在环境中找不到位。我尝试使用

因为 _bit 出现在 LOCAL 子句中，但这提供了类型不匹配，因为 _bit 是 ident 类型而不是 int 或 Z 类型。我想知道我应该如何使用我本地定义的值来调用其他函数，任何帮助将不胜感激。

VST 1.7，Coq 8.5pl2。

我有一个全局数组processesQVars我调用了一个函数来进行就地修改，将 SEP 条件从

将 Int.repr 调用数组作为声明的processesQVals_contents变量，以

我遇到的问题是我试图通过forward_call调用这个数组上的另一个函数。该策略产生了这个（显然无法证明的）目标。功能规范的前提条件如下，然后是不可证明的目标：

是否必须更改前置条件中的 SEP 子句，或者有没有办法更改对forward_call的调用来处理它？

谢谢

我正在使用 VST v1.7。

有没有人证明一个 int 等于一个字符数组？沿着这些思路：

除了打破field_at抽象来证明这一点之外，还有其他解决方案吗？

以下是 C 中的示例代码。

我使用可验证的 c (vst) 编写了它的功能规范，但在验证结束时我遇到了错误“typecheck_error (deref_byvalue tint)”。任何人都可以告诉我如何编写上述 c 函数的正确 founc 规范吗？关键是如何编写全局变量的 SEP()。

（这里是错误的，请纠正我）

以 VST 项目中的示例为例，reverse.c 文件有一个这样的链表：

它的分离逻辑写成：

其中 LS 定义为：

我的问题是如果我有一个双链表，如何编写其对应的分离逻辑。例如：这样的双链表：

那么，“”应该是什么SEP (lseg LS?? sh (map Vint contents) p nullval)？

我试图了解 VST 如何处理（可寻址）局部变量，所以我编写了这个函数：

然后我尝试使用以下规范对其进行验证：

一切都很顺利，只需使用 ( forward) 直到我留下来证明以下内容的 return 语句

这似乎应该是无法证明的（请注意，我刚刚申请forward到这一点）。我期待一些规范说明在局部变量被释放后堆是空的，即emp |-- emp。

有什么地方可以让我获得更多关于这方面的信息吗？

谢谢！

附加信息：我挖掘了FF后置条件的来源，它来自typecheck_expr，特别是以下情况Evar：

除非我读错了，否则这似乎表明您不能按值访问局部变量。这只是一个疏忽吗？或者语义中有什么东西可以防止这种情况发生？

似乎这tc_expr仅限于对类型上下文的了解，因此无法安全地“类型检查”需要了解堆状态的表达式，例如作为 while 循环条件的指针取消引用。为什么会这样，我是否有可能证明正确的循环，例如：

我认为 while 循环可以有选择地通过一种变体来证明tc_expr，它允许通过考虑堆上下文和键入上下文来取消引用指针。我怀疑这种想法是循环条件应该是一个“纯”表达式，但我最终很好奇这是否真的是一个必要的约束。

PS我意识到我可以将其重写为for循环。我的问题仍然存在，知道 VST 允许我证明这种循环，尽管语法不同。