Frama-C 中的模型变量

Question

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

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

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

甚至

//@ model integer x = 0;

导致解析错误。

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

谢谢， 爱德华多

Answer 1

正如 ACSL 手册“实施”版本的第 11 页所述，以红色字体编写的功能在 Frama-C 中尚不可用。实际上，在 Nitrogen 中，既没有实现模型变量，也没有实现模型字段。