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

Question

我在Mac上使用Frama-c的N版本，似乎不能使用ACSL手册中记录的" set“逻辑，例如，我不能像"//@ ghost set someSet;”那样声明ghost变量。

不管怎样，frama-c程序总是会抱怨声明set的那一行中存在语法错误。

我还尝试了"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变量。

在您的例子中，看起来部分实现的特性并不是集合(快速查看后，它似乎是在前端实现的)，而是ghost代码，它目前只能使用C结构和类型。

或Mac版本(我下载的是英特尔二进制版本)已经过时了，我应该编译最新的源代码吗？

此时您拥有最新版本。