不承认具有Frama-c的RTE插件：“-rte-无符号-ov”

Question

我是新来的。我正在尝试使用rte插件生成注释。通过查看链接1，我尝试使用以下命令生成注释：

frama-c -rte -rte-未签名-ovtest.c

其中我的test.c包含

int main(void){
  signed char cx, cy, cz;
  cz = cx + cy;
  return 0;
}

我从2节2.1.2中复制了代码。我希望rte将生成以下注释并修改test.c文件：

/*@ assert rte: signed_overflow: -2147483648 <= (int)cx+(int)cy; */
/*@ assert rte: signed_overflow: (int)cx+(int)cy <= 2147483647; */

但是，它没有生成任何注释(没有修改test.c)，而且frama-c无法检测选项“-rte-unsigned”。它向我展示了

[kernel] User Error: option `-rte-unsigned-ov' is unknown. 

我还尝试了命令"frama-c -rte test.c“，但是没有生成注释。我已经尝试过19.0和18.0版本的frama。

如果有人能帮我找出我错过了什么，那就太好了。谢谢。

1

2

Answer 1

这里有两个问题，一个是您对Frama会做什么的理解，另一个是https://frama-c.com/rte.html提供的文档中的问题。

让我们从第二点开始:文档已经过时了，您可能应该在https://github.com/Frama-C/Frama-C-snapshot/issues上打开一个问题。RTE手册为您提供了第2.3节中选项的新名称，即-warn-unsigned-overflow。

对于第二点，Frama永远不会修改您的输入文件。相反，您可以要求它重新打印它使用选项-print解析的代码源。您还可以使用选项-ocode <file>将此结果重定向到一个文件中。在RTE插件运行之后，您必须这样做，因此需要使用-then操作符。

因此，完整的命令行应该是

frama-c test.c -rte -warn-unsigned-overflow -then -print -ocode <yourfile>