问题标签 [frama-c]

我正在尝试使用 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 插件：

分析TU_core.ml

和 ：

分析TU_register.ml

和 ：

分析TU_options.ml

最后是makefile：

所以，当我用 make 命令编译它时，我实际上得到了：

我当时认为这是因为编译器不知道“out”这一事实，因此我将“out”替换为“chan”。顺便说一句，我遇到了同样的错误。

开发人员指南教程的代码中未定义“out”这一事实最终让我认为这个错误不是我想的那样......

你有没有遇到过？如果是，您是如何处理的？

我是 Frama-c 的新用户。我刚刚使用 Ocaml 编译器 4.01.0 在我的 Fedora 14 系统上安装了 Neon-20140301 以及为什么要安装 2.34。

在无GUI模式下，安装成功。

但是，当我尝试从 why2.34 运行一些示例时，我收到了如下几个错误： 似乎存在兼容性问题。

我的源代码 ac 中的主要方法接受 2 个参数：一个是文件名，另一个是整数。我像这样运行它：

但是当我尝试使用带有 frama-c 的切片时

Framac 抛出一个错误，说它找不到文件 3 ???

当我输入 filename1.txt_3 并在代码中分别提取它们时，我还尝试了其他选项，但即便如此，frama-c 也不喜欢它。它抱怨它找不到文件filename1.txt_3。

请让我知道如何在运行 Frama C 时向源发送多个参数

我正在尝试使用 Frama-C 来验证包括动态内存分配的 C 代码的安全属性。当前版本的 ACSL 规范语言 (1.8) 似乎能够表达很多关于动态分配内存的内容。然而，大部分这些东西还没有在 Frama-C Neon 中实现。

假设我们采用以下代码片段：

因此，main 分配了两个内存块，并将指向它们的指针传递给函数测试。测试释放 p 指向的块，但不释放 q 指向的块。假设我想证明在测试结束时，指针 q 仍然有效。我将如何进行？

看来我必须自己建模堆：公理化一些谈论堆的谓词，并使用它们来指定 malloc 和 free，模仿 ACSL 的未实现部分。最简单的方法是什么，以便我可以验证上面的示例？

我想根据 calculus.ml 代码生成由 Frama-C 生成的所有先决条件，这些先决条件存储在一个表中。我主要有兴趣获得转换为逻辑公式并发送给求解器的初始谓词。这可以做到吗？请帮我打印发送给求解器的初始谓词。我正在尝试的代码如下：

我从 Frama-c 得到一个后向切片，但看起来它是一个静态切片而不是动态切片。

frama-c 中是否有特定选项来获得动态后向切片？

我正在尝试使用 frama-c 验证以下代码

证明者无法证明main没有赋值，这是有道理的，因为main通过函数f赋值给 *p 。但是，我应该如何在 \assigns 子句中说明这一点，因为p是局部变量并且不能在注释中访问。

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

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

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

我的 frama-c 和 Why3 版本：

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

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

我试图在这个例子中证明返回值将是 0（如果 8 不在数组中）或 1（如果 8 在数组中）。

我创建了前置和后置条件：

和循环不变量，因为 Frama-C 基于 Hoare Logic：

我很确定我在尝试使用 forall 并存在的地方遗漏了一些东西。我花了几个小时试图理解，如何正确检查，是否在数组上分配了任何值，但我觉得我被困在这里。我真的很感谢你的帮助:)