问题标签 [frama-c]

在frama-c中编写函数的ACSL时，我希望全局变量数组满足要求，例如：

我想要一个大于 0 的所有元素，是吗？试了一下，还是不行，谁能告诉我怎么写？

非常感谢。

我想切片以下程序：

目前，Frama-C 在读取 后停止探索路径j，导致ERROR标签被切掉：

有没有办法将阅读j视为阅读未指定的值？我宁愿以编程方式（在 Frama-C 内部）执行此操作，而无需修改分析的源代码。

我正在运行 Frama-C Neon。

我正在学习如何开发 Frama-C 插件。在阅读了 Frama-C 开发人员手册并完成了 CFG 插件示例之后，我尝试编写一个基本脚本来打印 C 文件中的所有注释。我想出了这个：

即使输入文件具有 ACSL 注释并且从不打印注释 ID，它也总是说列表为空。我究竟做错了什么？

编辑：

带有以下代码的示例：

并使用以下命令调用 frama-c：

给出以下输出：

我正在 Frama-C 中开发一个插件。我想解析一个xml文件。我安装了软件包 libxml-light-ocaml-dev，但在编译时出现错误“Unbound module Xml”。我不知道如何继续使 Frama-C 可以看到包。或者我应该使用另一个包？

我正在尝试在 printf 调用中对以下程序进行切片：

但是，价值分析插件会给出以下消息：

foo.c:9:[value] 函数调用表达式参数 (char const ) (argv + 2)的评估中的非终止，

切片的程序是空的！这是 Frama-C 中的错误/功能吗？还是我做错了什么？

这是一个完整的跟踪：

我将尝试在 C 中的一个项目上使用值分析，但该项目包含一些.c文件，我们可以在其中找到汇编代码。当我尝试在这些文件上启动 frama-C 时，汇编代码出现错误。

汇编代码是为摩托罗拉68040设计的，我在文档中看到，我需要使用选项-machdep来更改模块的分析平台，但是这个平台没有定义，所以我需要联系支持还是可以我将模块配置为忽略汇编代码？

第二个问题，关于 SpareCode 模块。我们可以配置模块，只查看死代码并保留备用代码（在过程的情况下）吗？

otherfile.c 的代码（无注释）：

使用 Ubuntu 14.04，我下载了 Neon Frama-C 发行版，并安装了所需的工具：labgtk、sourceview 等。我配置 Frama-C 没问题，但在构建时得到：

问题是

其中 Z 表示未导入的模块（我猜）。我不知道 Z 应该指的是什么，所以我无法尝试解决这个问题。

例如，当使用带有选项 -wp-out 的 Frama-C WP 时（使用 swap.c 示例）：swap.c

执行：

并输出：

它证明属性并生成一个文件夹，其中包含证明程序的属性所需的证明义务，但不是全部，只有那些发送给 Alt-ergo 的那些不会生成 Qed 证明的那些。

我了解 Qed 的目的是简化、证明琐碎的属性以节省证明者的时间和精力，但是是否可以让它生成所有的证明义务发送给证明者？也就是说，禁用 Qed 并让 Frama-C 生成对 alt-ergo 的所有证明义务？

我对价值分析模块的选项和一些扩展选项有一些疑问。

我使用命令：frama-c-gui -val -slevel 100 -plevel 300 -absolute-valid-range 0x00000000-0xffffffff -metrics -metrics-value-cover -scope-def-interproc -main MYMAIN CODE/*.c

• 在一个文件上，-metrics给我 3goto一个没有的函数，goto计算如何？

• 什么是“覆盖率估计 = 100.0%”，-metrics-value-cover我得到一个介于 80% 和 100% 之间的值，一开始我认为当我有死代码时得到 <100%，但是当我得到 100% 时我有死代码，所以我认为得到100% 如果源文件中的所有函数都被分析？

• 我想157 stmts in analyzed functions, 148 stmts analyzed (94.3%)这意味着我的项目上有死代码，是吗？

• 使用选项-scope-def-interproc我收到 32 个警告（没有 62 个）但在网站上，我们可以阅读（在范围文档中）

  因此，用户应仔细检查值分析发出的警报。

所以我需要验证所有 62 个警告还是仅通过此选项获得 32 个？

我对最后一个 Frama-C 版本的 ACSL 规范有一些问题。
我尝试了很多方法来声明一对实数，但都没有奏效。这是一个按问题说明的小例子：

这使 ：

[内核] 用户错误：意外令牌 '('

最后，我想有一个代码接近：

有人看到错误在哪里吗？我发现 ACSL 文档在类型声明上非常含糊......

非常感谢您的回答。

此致，

尼莱克斯。