带有 Frama-c 的 RTE 插件：无法识别“-rte-unsigned-ov”答案

【问题标题】：RTE plugin with Frama-c: "-rte-unsigned-ov" is not recognized带有 Frama-c 的 RTE 插件：无法识别“-rte-unsigned-ov”
【发布时间】：2019-07-13 16:03:33
【问题描述】：

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

frama-c -rte -rte-unsigned-ov test.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-ov”。它告诉我

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

我也尝试了命令“frama-c -rte test.c”，但没有生成注释。我尝试过使用 19.0 和 18.0 版本的 frama-c。

如果有人可以帮助我找出我缺少的东西，那就太好了。谢谢。

[1]https://frama-c.com/rte.html

[2]https://frama-c.com/download/frama-c-rte-manual.pdf

【问题讨论】：

标签： c verification frama-c rte

【解决方案1】：

这里有两个问题，一个是您对 Frama-C 功能的理解，另一个是 https://frama-c.com/rte.html 上的文档。

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

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

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

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

【讨论】：