1

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

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

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

甚至

//@ model integer x = 0;

导致解析错误。

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

谢谢,爱德华多

4

1 回答 1

2

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

于 2012-04-27T08:00:38.607 回答