问题标签 [frama-c]

我想知道 PDG 中曲线或圆弧的含义。哪些是数据依赖，哪些是控制依赖等等。

是否有一个 frama-c 插件来输出过程间数据流/指向图？

我知道切片器插件中的 -pdg 将包​​含此信息，但想知道我是否可以单独获取它。

我正在使用 Frama-C 来计算 C 程序的一部分。我希望切片程序看起来像没有代码转换的原始程序。然而，在生成的切片中，我总是有 goto 语句和标签。我使用命令：

我在 Cygwin 下的 Windows 机器上从最新的 Oxygen 版本编译了 Frama-C。

在使用 Frama-C 版 Oxygen 的程序切片器时，我遇到的问题是生成的切片使用了未声明的变量。我之前搜索过该主题的现有帖子，发现： http ://bts.frama-c.com/print_bug_page.php?bug_id=806

那里提到该错误已在 Frama-C 的 Nitrogen 版本中修复。也许这种变化并没有转移到氧气上？就像在现有帖子的描述中一样，它只发生在只有一个语句的块中。我无法附上示例源代码，因为它来自客户项目。

我有一些问题要决定如何告诉Frama-C 使用哪些包含文件。我通常添加选项：

为了获得 Frama-C 的标准规格。但我经常需要一些不在 Frama-C 库中的东西。

例如，我要分析的源文件之一使用了定义在 中的宏<sys/wait.h>，但因为 Frama-C 有自己的frama-c/libc/sys/wait.h，所以不包括 gcc 文件。不幸的是，Frama-C 没有定义宏，并且定义最终丢失了。当然，我不想更改源文件！

my_libc/sys/wait.h我正在考虑使用包含 Frama-C 文件的文件构建一个本地目录，并且我可以在其中复制 GCC 文件中缺少的内容。

然后我会使用：

但我对我的解决方案有点担心，因为从 GCC 包含文件中提取定义可能非常棘手......

你怎么看？这似乎是个好主意？您对更好的组织有什么建议吗？

我想知道 Frama-C 是否实现了某种与指针相关的类型检查。例如，考虑以下情况：

有没有和上面类似的精神？

看 ACSL 手册，有很多方法可以检查内存和指针的使用情况（其中一部分是在 Frama-C Oxygen 中实现的）。不过，我还没有找到任何通用的支持来处理类型信息。是否有我们可以用于此目的的 frama-c 插件？

谢谢，爱德华多

我正在寻找 C 语言的正向切片工具。当我在谷歌搜索时，我没有找到任何结果。

我本来希望访问 Wisconsin Program-Slicing Tool 1.1 版，但该工具并未分发。任何其他工具能否提供正向切片 C 程序的功能？

当我使用 frama-c 分析我的 c 程序时。似乎在 frama-c 的影响插件中存在错误。这是我的程序。

我想找到受变量“全局”影响的所有状态。显然，语句“结果 += 100;” 在与变量“global”相关的“if condition”范围内，所以语句“result += 100;” 应该是高光。但是，运行结果似乎不正确。

我正在尝试使用 frama-c 的 WP 插件来证明一个简单的断言。C 代码是从 Targetlink 查找表生成的。我的目标是为函数提供足够的注释，以便我可以使用生成的合约来证明调用程序的属性。作为第一步，我在函数开头附近编写了一个断言，它将常量与从取消引用的指针获得的值进行比较，请参见以下示例。

有人可以提示我需要哪些注释才能成功证明吗？通过查看 Coq 证明义务，我发现没有用于重写条款所需的“addr_of_data”或“access”等操作的公理。断言中引用的全局变量的信息也丢失了。

BR，哈拉尔

我试图证明数组的量化断言并遇到了一些问题。考虑以下小程序：

我正在使用“类型化”内存模型：

frama-c-gui -wp -wp-qed -wp-byreference -wp-model 'Typed' -main test Test.c

由于某种原因，“要求”不成立，因此可以证明所有断言，即使是 1==2。为了克服这个问题，我直接在函数体中分配了全局变量：

这里 forall 成立，但存在不成立。只有当我在它之前添加断言“p [1] == 3”时，存在才成立。证明这种存在数组属性缺少什么？我需要这个来表达数组条目上搜索循环的循环不变量。

谢谢，哈拉尔