问题标签 [frama-c]

我在我的系统中安装了 frama-c。

它是做什么的，它将我的所有代码转换为具有 C.. 的所有隐式转换的更扩展的形式。

(例如)
//我的实际代码

//Frama-c转换后的代码

现在我的疑问是， 在创建对象程序之前， C 编译器是否会进行所有隐式转换？

或者

在创建目标程序期间，这些隐式转换是否并行完成？

或者

它依赖于实现吗？如果是这样，为什么？

我希望对 Frama-C 开源项目进行一些试验，并希望在 Windows 7 机器上安装这些工具。看起来以前的版本有适用于 Windows 的二进制安装程序，但最新版本 Nitrogen 只有可用的源代码。该项目的网站frama-c.com说这些应该是可用的，但我没有在他们的下载页面上看到它们。二进制安装程序在其他地方可用吗？

我使用 Frama-C 工具来生成这个程序（main.c）的依赖图。

命令是：

结果是 我的问题是为什么语句“m=m*i;”，“m=m%10000”不映射到节点。结果似乎不对，因为代码中有三个循环。

我使用 frama-c 工具来分析下面的代码。

cmd是

我的问题是关于控制依赖。圆圈节点是什么意思？我试着解释一下“while”节点，也许它代表一次循环，因为一个循环从“i<100”开始，所以存在控制依赖（“i<100”-----o“while” ）。我猜对了吗？但是“中断”节点是什么意思？我猜那个节点“goto __Cont;” 与“休息”有关；“else”块中的语句。
我想我脑子里没有清晰的抽象模型来完整准确地理解控制依赖。你会帮助我或给我任何建议吗？非常感谢提前道。

我是 Frama-C 的新手用户，对指针断言有一些疑问。

考虑以下涉及的 C 片段：

• 两个相关的数据结构Data和Handle，st Handle有一个指向Data的指针；
• 数据中的“状态”字段，指示某些假设操作是否已完成
• 三个函数：init()、start_operation() 和 wait()；
• 使用上述方法的 main() 函数，并包含 6 个断言 (A1-A6)

现在，为什么 A5 和 A6 不能用 WP 验证程序断言（“frama-c -wp file.c”）由于 start_operation() 上的最后一个“ensures”子句，它们不应该成立吗？

我究竟做错了什么？

最好的，

爱德华多

我在 Mac 上使用的是 Frama-c 的 Nitrogen 版本，并且似乎无法使用 ACSL 手册中记录的“设置”逻辑，例如，我不能像“//@”中那样声明幽灵变量幽灵集<整数> someSet;"。

无论如何，frama-c 程序总是在声明集合的行中抱怨语法错误。

我也尝试用“Set”代替“set”，用其他类型代替“integer”（例如“char*”）并指定“//@ open set;” 导入模块。

也许我需要指定一些命令行选项？执行“frama-c -kernel-help”目前尚不清楚那会是什么。

或者 Mac 版本（我下载了 Intel 二进制版本）已经过时了，我应该编译最新的源代码？

谢谢，最好的问候，

爱德华多

模型变量在 Frama-C 手册中进行了描述（在规范和“实现”版本中）。

但是我无法解析一个简单的片段，例如手册中的片段，例如。

甚至

导致解析错误。

真的支持模型变量吗？如果是这样，我做错了什么？我使用的 frama-c 版本是 MacOS 上的 Nitrogen。

谢谢，爱德华多

我正在尝试使用 frama-c 值分析器来评估实际上是线程化的 C 代码。我想忽略任何可能发生的线程问题，只检查单个线程的可能值。到目前为止，这是通过将入口点设置为线程开始的位置来实现的。

现在我的问题是：在一个线程中，我读取由另一个线程写入的值，因为 frama-c 不（也不应该？）考虑线程（当前）它假设我的变量在某个广泛的范围内，但我知道范围实际上要小得多。是否可以告诉值分析器这个变量的值范围？

例子：

这里 frama-c 检测到 x 是易失的，因此具有范围 [--..--]，但我知道另一个线程将写入 x 的内容，我想告诉分析器 x 只能是 0 或 1。这对frama-c是否可行，尤其是在gui中？

在此先感谢基督教

假设有两个外部函数 init() 和 revoke()。Init() 返回“有效”值，revoke() 使它们无效。我想验证 use() 仅使用已初始化但未撤销的值。我不知道如何将此属性描述为谓词（想想随机会话 ID）或其他方式。

我正在尝试安装 ocamlgraph 作为 frama-c 的要求。当我安装 ocamlgraph 并运行 make 时，我收到以下编译错误：

我在 Ubuntu-10.04 上运行并尝试了 ocamlgraph-1.6 和 ocamlgraph-1.8.2 版本，但出现了相同的错误。我机器上的ocaml版本是ocaml-3.11.2。

谢谢