ACSL 设置逻辑/frama-c 语法错误

Question

我在 Mac 上使用的是 Frama-c 的 Nitrogen 版本，但似乎无法使用 “设置”逻辑，如 ACSL 手册中所述，例如，我不能声明 一个幽灵变量，如“//@ ghost set someSet;”。

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

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

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

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

谢谢，最好的问候，

爱德华多

Answer 1

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

• 该功能必须是 ACSL 语言的一部分。
• 必须是made available by the current Frama-C front-end。并非 ACSL 语言的所有功能都立即在前端实现。
• 您打算使用的插件必须利用它。

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

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

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

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

您目前拥有最新版本。