问题标签 [frama-c]

我需要在 ACSL 中编写一个归纳谓词，说明一个链表是另一个链表的子表。

谓词的签名应该是这样的：

所以基本上我想要一个谓词来说明状态 L1 上的链表 l 是同一个链表 l 的子列表，但在这种情况下是状态 L2。

我是 Frama-c 的新手，我想了解这个简单示例有什么问题：

在此示例中，Frama-c (WP + Value) 不会证明函数合同中的分配子句，我不明白为什么。任何帮助将不胜感激 =)

我正在尝试在 cygwin 中安装 frama-c 并收到以下错误，但我无法解释它们。你能帮我解释一下，或者给我一个链接到我从哪里得到信息吗？

请注意，coqc 和 ocaml 都是最新版本

我需要为将指针作为输入的函数的依赖关系编写 ACSL 规范，并在指针不为 NULL 时使用其内容。我认为这个规范是正确的：

但我宁愿避免这些行为，但我不知道这是否正确（和等效）：

即使可能是，我可以*p在正确的部分使用吗？\frompNULL

我想访问由 Frama-C 工具创建的抽象语法树 (AST)。是否有插件或任何其他支持来访问 Frama-C 中的 AST？

我想分析一个大型项目中的文件以使用 Frama-C 创建程序依赖图，但不断收到奇怪的错误，例如：

/usr/include/bits/fcntl-linux.h:305:[kernel] 用户错误：数组长度为零。此扩展程序不受支持

如果我尝试使用 frama-c 提供的 libc 实现，由于缺少 sys/file.h 等头文件，编译会失败。

我正在尝试使用 GCC 版本 4.8.1 分析 Lynx 项目中的文件，特别是 src/WWW/Library/Implementation/HTTP.c 中的文件

我真正需要的是能够为这个源文件生成一个 PDG（它当然有各种依赖项），但我认为如果我可以通过跳过未定义的函数来获得一个有点不完整的图表，那将是一个很好的第一步。

我有这个功能可以打印出偏移图中的值：

现在，我想将值放入一个字符串变量中，以便出于我的目的对其进行转换。我替换Format.fprintf fmt了，Printf.sprintf但它不起作用。编译错误：

我想知道是否可以使用 Frama-C 进行某种前向条件切片，并且我正在使用一些示例来了解如何实现这一点。

我有这个简单的例子，它似乎导致了一个不精确的切片，我不明白为什么。这是我要切片的功能：

如果我使用这个规范：

然后 Frama-C 使用“f -slice-return”标准和 f 作为入口点返回以下切片（精确）：

但是当使用这个规范时：

然后所有指令（和注释）仍然存在（当我等待这个切片被返回时：

)

在最后一种情况下，切片是否不精确？在这种情况下，可能是什么原因？

问候，

罗曼

编辑：我写了“else if(a != 0) ...”但问题仍然存在于“else ...”

我想查询 Frama-C 中的值分析插件以获取获取其值的说明。对于每个数组，它返回整个数组的取值范围。例如，如果指令是array[i] = 1;，我从值分析插件中得到了 result = {1}for 。array[i]现在，例如array[i]，我想i从值分析中获取变量名称及其值。

下面是我的代码示例

有人可以帮我吗？提前非常感谢。

我的最后一个问题（Understanding Frama-C slicer results）是一个精确的例子，但正如我所说，我的目标是知道是否可以使用 Frama-C 进行一些条件切片（向前和向后）。可能吗？

更准确地说，我无法获得该程序的精确片段：

在这种情况下/在一般情况下，是否有可能通过使用良好的参数/选项来获得我想要的？