Frama-C中的模型变量

Question

模型变量在Frama-C手册中描述(在规范和“实现”版本中)。

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

//@ model set<integer > forbidden = \empty;

甚至是

//@ model integer x = 0;

导致解析错误。

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

谢谢，爱德华多

Answer 1

正如ACSL手册的“实现”版本的第11页所述，以红色字体编写的功能在Frama-C中尚未提供。事实上，在氮气中，既没有实现模型变量，也没有实现模型场。