问题标签 [why3]

我正在尝试用 krakatoa & jessie (why-2.33) 为 Windows (Cygwin) 编译 why3ide (why3-0.81)。一切都很好，除了我不能让右下角的文本框显示符号（它总是空的），而且每次我尝试选择要证明的项目时都会收到错误（在图片中突出显示）。

图片：https ://dl.dropboxusercontent.com/u/39984835/why3ide/error_capture.jpg

这是这个错误：

如何调试此错误？（我是 OCaml 的新手）

format.ml 文件在这里：
cygwin/lib/ocaml/format.ml

引用引入前提转换的文件在这里：
why3-0.81/drivers/gappa.drv
why3-0.81/src/ide/gmain.ml
why3-0.81/src/transform/introduction.ml
why3-0.81/drivers/mathematica.drv

PS我试图为这篇文章添加why3和why3ide标签，但我的声誉还不够。

我有以下示例代码：

但是 Frama-C / Why3 无法证明代码中注释的“要求”之一。.Why 文件说明以下内容：

为了学习，我的问题是：

1）该前提条件有什么问题？

2）基于 .Why 文件中的输出，我应该采取什么方法来找出问题所在？

3）有人可以指点我学习如何调试我的函数合同的资源吗？

编辑：

我使用以下标志运行 Frama-c：“-wp -wp-rte -wp-fct f_mount_temp”我没有从其他地方调用这个 f_mount_temp。我运行 Frama-c 直接检查这个 f_mount_temp()。

现在对我来说更清楚了，它可能是导致先决条件失败的额外断言。处理的函数契约如下，注释指示每个断言的状态：

-wp-rfe 标志添加的内联断言是：

我正在尝试使用 alt-ergo 证明器在 frama-c 上运行测试文件。但是，我在使用 alt-ergo 时遇到了以下错误。所有其他的 frama-c 检查都很好。我知道问题不在于测试文件。

我在windows机器上并通过cygwin以管理员模式执行所有安装我得到了frama-C Neon并安装了它./configure & make & make-install，安装成功（所有frama-c检查都通过了我的测试文件）

我从http://alt-ergo.ocamlpro.com/download.php获得了以下版本的 alt-ergo Linux x86_64 二进制文件：alt-ergo-0.95.2-x86_64 。我选择了这个版本，因为 frama-c 文档要求版本 0.95。

我使用以下说明安装 alt-ergo ( https://www.lri.fr/~marche/MPRI-2-36-1/install.html )

安装 Alt-ergo

最简单的方法是获取alt-ergo的二进制文件。下载名为“Linux x86_64 binary”的文件然后：

打电话时，which但 frama-c 和 alt-ergo 有正确的路径

我也安装了Why3，它检测到了ergo prover

编辑

我使用在线示例创建了以下 test.mlw

运行 alt-ergo 会导致：

有任何想法吗？

我已经安装了frama-c 和why3，但是当我尝试启动frama-c 时，jessie3 出现错误。

我没有找到有关 camlGzip 的任何信息，因此它可能是任何配置文件中的错误（它可以是 camlzip），但我没有找到它的声明位置。

编辑：我试图在 Jessie3.cmxs 中修改 camlzip 中的 camlGzip，但是当我启动 frama-c 时它会产生分段错误

我的 frama-c 和 Why3 版本：

我在 Mint17 虚拟机上工作，每个程序的 ./configure 和 make 都没有错误

我希望有人已经遇到过这个问题并且可以帮助我

我正在尝试使用Why3 的​​ Z3 后端来检索模型，然后这些模型可用于派生显示程序错误的测试用例。然而，Z3 版本 4.3.2 似乎无法回答sat任何 Why3 目标。看起来Why3 使用的一些公理化定义以某种方式混淆了 Z3。例如，下面的例子（这是 Why3 生成的一小部分）

结果timeout如下命令行：

另一方面，将定义更改为

会给我一个模型（看起来很合理）

但是如果我尝试添加原始Why3文件中存在的下一个公理，即

Z3 再次回答timeout。

Z3的配置中是否缺少我的东西？此外，在以前的Why3 版本中，有一个选项MODEL_ON_TIMEOUT，允许在这种情况下检索模型。尽管不能保证这是一个真实的模型，因为 Z3 无法完成检查，但实际上这些模型通常包含我需要的所有信息。但是，我在 4.3.2 中没有找到类似的选项。它还存在吗？

更新最后一个公理Abs_pos是错误的（我在此处发布之前对Why3 的​​输出进行了一些玩弄，最终粘贴了该问题的错误版本）。现在已修复。

我正在尝试在 Windows 环境中使用cvc4带有Frama-c wp插件的证明者。Why3我有frama-c并why3安装在我的系统上。Why3 被正确配置为包含 cvc4 作为证明者：

我使用 frama-c Wp 插件使用以下命令生成与我的 .c 文件（具有 ACSL 规范的 C 源文件）相对应的为什么 3 格式（.why）文件：

swap_Why3_ide.why上面的命令在C:/Users/user/temp/typed目录 中生成一个文件。

当我尝试使用with作为证明者来证明生成swap_Why3_ide.why文件中的理论时，它失败并出现以下错误：why3cvc4

我在 linux 环境中执行了相同的步骤，并且why3能够执行证明程序：

谁能建议如何在 Windows 上执行Why3？

美好的一天，自动扣款和验证黑客！

为了更深入地了解WhyML 究竟如何为 ACSL 注释的 C 程序提供证明，我试图手动“重现”Why3 对 WhyML 程序所做的工作，同时将其转换为 SMT 逻辑并将其输入 Z3 证明程序。

假设我们有以下 C 片段：

我正在尝试将其编码为 SMT 逻辑，如下所示：

Z3 给出“未知”。

这可能是因为在指定 set_a_i 函数时使用了量化。但我看不到其他方法来指定它。

我知道以下陈述：

• SMT 求解器通常不能（或以不好的方式）处理数组上的量化。
• 如果我提供前后条件和循环不变量，WhyML 能够证明这样的程序。
• 即使后端设置为 Z3，WhyML 也能够证明此类程序，因此 SMT 求解器本身不是问题。
• WhyML 可以生成 z3 smt 文件，但要理解它是一件很辛苦的事情，部分原因是由于 whyML->smt 翻译的自动性质（例如，它不保留变量名）

我阅读了几乎所有为 WhyML、Frama-C WP 插件和 Z3 提供的材料。我还阅读了几篇关于验证 C 代码的论文，但没有发现任何关于 C --> SMT 翻译技术的文章。

我应该学习哪些材料来获得这种理解？您能否提供见解和/或链接到描述这种将命令式代码转换为多排序一阶逻辑的机制的论文。

我将不胜感激任何评论。谢谢！

祝你好运，叶夫根尼。

我正在使用 Frama-C、Alt-Ergo 和 Why3 进行系统验证。在 Frama-C 中生成并发送到 Why3 的​​一项证明义务如下所示（这是 Why3 版本）：

我想知道什么t_1[a_5 <- x]意思。

访问之前是xto的分配吗？a_5t_1[a_5 <- x]

假设我们有以下带注释的 C 代码：

Z3 和 Alt-ergo 都无法证明 assert final_a 和后置条件；Z3 也不能证明循环不变；

Alt-Ergo 的输出：

Z3 的输出：

什么不见​​了？

是否可以对 ACSL 中定义的归纳谓词使用归纳？

考虑ACSL 手册中的以下示例：

我试图证明以下引理：

Alt-Ergo 在这里失败了，所以我求助于手动 Coq 推理：

但是当 I 时Search P_reachable，我发现只生成了两个公理：

并且没有感应原理。所以我不能申请induction P_reachable或destruct P_reachable。

我使用frama-c版本 Sodium-20150201 的 WP 插件。

要重现，您可以运行frama-c -wp -wp-rte -wp-prover coqide file.c，其中file.c包含List和reachable定义和next_null_reachable引理。