带有 Frama-c 的 RTE 插件:无法识别“-rte-unsigned-ov”
RTE plugin with Frama-c: "-rte-unsigned-ov" is not recognized
我是 frama-c 的新手。我正在尝试使用 rte 插件生成注释。
通过查看 link [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。
如果有人能帮我找出我遗漏的东西,那就太好了。谢谢。
这里有两个问题,一个是您对 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 将永远不会 修改您的输入文件。相反,您可以要求它 pretty-print 返回它使用选项 -print
解析的代码源。您还可以使用选项 -ocode <file>
将此结果重定向到一个文件中。您必须在 RTE 插件具有 运行 之后执行此操作,因此需要 -then
运算符。
因此,您的完整 command-line 应该是
frama-c test.c -rte -warn-unsigned-overflow -then -print -ocode <yourfile>
我是 frama-c 的新手。我正在尝试使用 rte 插件生成注释。 通过查看 link [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。
如果有人能帮我找出我遗漏的东西,那就太好了。谢谢。
这里有两个问题,一个是您对 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 将永远不会 修改您的输入文件。相反,您可以要求它 pretty-print 返回它使用选项 -print
解析的代码源。您还可以使用选项 -ocode <file>
将此结果重定向到一个文件中。您必须在 RTE 插件具有 运行 之后执行此操作,因此需要 -then
运算符。
因此,您的完整 command-line 应该是
frama-c test.c -rte -warn-unsigned-overflow -then -print -ocode <yourfile>