2

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

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

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

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

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

谢谢，最好的问候，

爱德华多

4

1 回答 1

2

ACSL 是一种独立于 Frama-C 存在的注释语言，尽管有一些相同的人在两者上工作。从在 Frama-C 插件中使用 ACSL 的角度来看，定义/实现分为三个级别，您需要全部三个级别才能使用一个功能：

  • 该功能必须是 ACSL 语言的一部分。
  • 它必须由当前的 Frama-C 前端提供。并非 ACSL 语言的所有功能都立即在前端实现。
  • 您打算使用的插件必须利用它。

相同区别的另一种解释是here。

我不能像在“//@ ghost set someSet;”中那样声明一个幽灵变量。

在您的情况下，部分实现的功能似乎不是那么多集（快速浏览后似乎在前端实现）而是幽灵代码，目前只能使用 C 构造和类型。

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

您目前拥有最新版本。

于 2012-03-31T13:36:00.407 回答