问题标签 [frama-c]

在 Frama-C 中，是否可以自由指定基本类型的大小？

我的目标 TMS320F2808 DSP 具有 16 位字节。char、short 和 int 类型都是一个字节，long 类型是两个。

到目前为止，如果可能的话，我无法看到如何为 Frama-C 指定这些尺寸。

当使用一些基准运行 Frama-C 值分析时，例如susan在 中http://www.eecs.umich.edu/mibench/automotive.tar.gz，我们注意到很多块被认为是死代码或无法访问。然而，在实践中，这些代码是在我们从这些块中打印出一些调试信息时执行的。有没有人注意到这个问题？我们如何解决这个问题？

当我使用fram-c 编写解析器时。我遇到了 Ast.get() 返回类型 Cil_types.file 但我需要 Cil.file 以供将来使用的问题。它们实际上具有相同的字段，但 ocaml 编译器只是不允许从 Cil_types.file 直接分配给 Cil.file。Ocaml 中是否有任何类型转换函数可以帮助我做到这一点。

Ps：我尝试将Cil_types.file的每个字段都赋值给Cil.file，但是递归出现同样的问题（不允许Cil.file.* = Cil_types.file.*）。非常感谢您的帮助！</p>

我正在尝试在我们客户的专有安全关键系统模块上应用 frama-c/jessie。正在分析的函数非常大（图像 700 未注释的行数）有很多条件语句以及复杂的（&&、|| 等）。

我在 Ubuntu VM 64 位机器上运行它时收到此错误消息。似乎错误 137 与内存大小等有关。但我不太确定。

非常感谢任何有关如何处理此错误的建议。

[

对于下面的 C 函数，我从 Alt-Ergo 收到最新版本的 Frama-c 的语法错误。

我不确定这个生成的行有什么问题：

正在分析的 C 函数

我正在尝试使用 Alt-Ergo 在相当复杂的功能上测试 WP 插件。不幸的是，我无法弄清楚下面给出的“基本”行为有什么问题。

这种行为应该是正确的，因为除了第一个条件语句的 else 部分之外，没有其他地方 tenumRMode 被更新。

奇怪的是，如果我任意评论某些行，我总是从 Alt-ergo 获得“有效”。

任何意见？

对于那些在 Windows 上编译 C 的人来说，这是一个简单的问题！

我想在 Windows 8 上使用最新版本的Frama-C C 静态分析器及其 GUI。据我所知，具有 Windows 安装程序的最新版本是 Boron，它已有 3-4 年的历史。所以看起来我需要自己编译它（版本 Fluorine 3）。但是，我在最初的几个步骤中磕磕绊绊。

Frama-C Fluorine 3的快速启动编译说明在此处。

• 第 1 步：安装 OCaml。我已经从这里安装了 windows 版本。

• 步骤 1b：我相信步骤 1 安装了 Gtk 等等。

• 步骤 2b：运行：

  ./configure --prefix C:/windows/path/with/direct/slash && make && make install

关于这些说明的 4 件事让我感到困惑：

1. configure这是哪个文件？如果我打开 Cygwin 终端，它会让我进入用户的主目录，如果我运行./configure它，它会说没有这样的文件或目录。我认为它是指源中的配置文件之一，但有超过 10 个。

2. 究竟是什么C:/windows/path/with/direct/slash意思？请有人能给我一个很好的解释的真实例子吗？

3. 我应该在哪个目录中运行上述命令（步骤 2b）？

4. 我应该将提取的 Frama-C 源代码分发放在哪个目录中？（我应该src从存档中提取目录，还是需要所有内容？）

我要做的就是按照他们主页链接的“简短示例”，使用最新版本，在 Windows 8.1 上，我需要一个“绝对傻瓜”指南来这样做！

非常感谢

我正在使用 Cil_types 在 frama-c 中开发一个插件。该插件默认将 C 程序的 AST 作为输入（Cil_types.file）。我想得到这个文件的名字，但使用 Cil_types 我不能。我可以通过其他方式获得这些信息吗？

我已经从 frame-c 网站http://frama-c.com/download.html安装了硼版的 windows 安装程序

当我尝试运行 val 插件时，我收到关于未设置预处理器变量 CPP 的错误，如下所示：

使用 -cpp-command 我收到以下错误：

任何线索/建议？

我在指定对内部状态变量的访问时遇到问题，即那些仅由 getter 和 setter 访问的模块的本地变量。我曾尝试在setter函数的函数契约规范中使用getter函数，但是frama-c返回错误：

这是标题：

这里是来源：

我认为这是一个普遍的问题。在 ACSL 中是如何完成的？有没有人有类似问题的例子？

我使用 Frama-C Fluorine-20130601。

提前致谢

坦率

编辑： 重新阅读 ACSL 规范更仔细地向我揭示了 C 函数在规范中是不可能的，只有逻辑函数。我试图将 C 函数包装在一个逻辑函数中，但这也没有被接受，同样的错误消息。我最终通过一个幽灵变量对内部状态变量进行了建模，但我不确定这是否是体面的方法。