问题标签 [verifiable-c]

我正在学习使用经过验证的软件工具链 (VST)。我被困在证明一个简单的“if-then-else”块上。

这是 .c 文件：

我写了一个关于iftest()如下的规范：

证明步骤是：

Lemma body_iftest : semax_body Vprog Gtot f_iftest if_spec.Proof. start_function. name a _a. name r _r. forward. (*r=0*) simplify_typed_comparison. forward. (*if(E)*). go_lower. subst. normalize.

它产生一个假设：Post := EX x : ?214, ?215 x : environ -> mpred“then”子句不能通过“go_lower”和“normalize”继续。

我尝试用 VST 验证我的程序。我收到一条奇怪的错误消息：

对我来说，我将使用的函数签名似乎forward_call正是这里需要的（share * Z * Z * val * val）

但 VST 抱怨。我应该去哪里看？这里有什么不同？

顺便说一句，如果它有用，我的中间证明状态：1 集中子目标（未集中：1-0-0），子目标 1（ID 4026）

我很难证明一个简单的数组访问函数（文件 arr.c）：

翻译clightgen arr.c为（文件 arr.v）：

这是证明开始（verif_arr.v）：

执行forward（verif_arr.v 中的最后一行）后，我有以下目标：

这意味着False，所以我无法证明。然而，c 实现是微不足道的，证明才刚刚开始。

现在问题：

规范有什么问题，为什么它达到了一个无法证明的目标？

VST 版本：

CompCert 版本：2.4

Coq 版本：

在 Programming Logics for Certified Compilers 一书第 23 页的表达式中：

在我看来，既然 σ 代表整个列表 v，而 σ' 代表尾部，那么最后一个表达式应该是：listrep σ' (t, 0)。对吗，只是书上的错别字吗？

我有两个问题：

首先，如果我使用内联汇编编写 C 程序，我可以在 VST 中验证整个 C 程序吗？还是只有纯C程序可以验证？

其次，我尝试在 Ubuntu 12.04 上安装最新的 VST 和 Compcert，如http://vst.cs.princeton.edu/上所述，但在某些时候，在将 .v 文件转换为 .vo 文件时出现错误，并显示消息为形式：'不可能将“2”与“8”统一起来'。我认为这个错误是在制作compcert期间发生的，但我不确定。

然后我尝试使用本指南在 Ubuntu 14.04 上安装 VST：' http: //ninj4.net/2014/05/16/hello-vst-hello-verifiable-c.html '。我安装了与指南中相同版本的 Coq、OCaml 和 Menhir。后来当我在 vst 目录中运行 make 时，我遇到了与上面类似的问题。以下是我得到的输出：

以下是失败的引理的 data_at_lemmas.v 片段（我已标记第 429 行）：

顺便说一句，我尝试在 bash: 中运行以下命令 ./configure -toolprefix arm-none-eabi- arm-eabi -no-runtime-lib 并收到此错误消息： ./configure: 65: shift: can't shift that many 但是./configure -toolprefix arm-none-eabi- arm-eabi有效。这不是问题，因为我更改了 Makefile.config。

有关如何解决此问题的任何建议？我还不知道 Coq（我刚刚阅读了指南“Coq in a Hurry”，不过也使用过 HOL）。我有其他新系统，我可以尝试在其上安装 VST（如果有必要的话），即使我已经尝试了两次。

提前致谢。

现在我试图证明一个简单的数组访问过程（文件 arr.c）：

该文件arr.c被翻译为arr.v：

这是我证明的开头（文件verif_arr.v）：

战术之后entailer!.，我得到了：

现在的问题：

• 在规范set_spec中有一个前提条件'(array_at tint sh arr 0 100) (eval_id _arr)（这里'应该是反引号，这会破坏格式）。为什么这个陈述没有出现在假设列表中？

• 第一个子目标在我看来就像它试图取消引用数组的 0 单元格 (arr + 0)，它应该等于第一个关键单元格 (arr + key)。这与代码或后置条件无关，当然无法证明。这里出了什么问题？

我用：

VST 版本：

CompCert 版本：2.4

Coq 版本：

编辑：

后置条件的最后local ...一部分被证明是多余的。

我正在尝试将我的两个功能的证明组合成整个程序的证明：

在应用semax_func_cons战术之前，我有以下目标：

所以f_get用我证明的引理来消除似乎是合理的body_get。为什么战术失败？

该消息无济于事：

这次我证明函数调用其他。vars.c：

我的证明开始 - verif_vars.v：

这导致了目标：

我想它说明了函数调用不会改变arr内容，这对我来说很明显。

我能用这个目标做什么？哪种策略适用于此，该声明的确切含义是什么？我是否应该丰富pure0规范以某种方式指出它不会修改任何内容？

我的简单程序是vars.c：

我开始证明（文件verif_vars.c）：

最后有两个子目标：

• 第一个直接来自pure0_spec后置条件。但是我怎么能告诉 Coq 呢？
• 第二个目标可以简化（由admit. entailer.）为TT |-- emp。这似乎又是微不足道的，但仍然如何证明它（SearchAbout derives并且SearchAbout emp不显示任何一般引理）？

我使用：VST 1.5（2014-10-02 时为 6834P）、CompCert 2.4、Coq 8.4pl3（Jan'14）和 OCaml 4.01.0。

WITH构造只为最多 8 个变量定义。如何使用超过 8 个？例子：

=>

我使用：VST 1.5（2014-10-02 时为 6834P）、CompCert 2.4、Coq 8.4pl3（Jan'14）和 OCaml 4.01.0。