我是frama-c的新手,我正在尝试使用rte插件生成注释。
通过查看链接[1],我尝试使用以下命令生成注释:
frama-c-rte-rte无符号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
最佳答案
这里有两个问题,一个是你对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永远不会修改您的输入文件。相反,您可以要求它使用option-print
漂亮地打印出它解析的代码源。您还可以使用选项-ocode <file>
将此结果重定向到一个文件中。必须在RTE插件运行后执行此操作,因此需要使用-then
运算符。
因此,完整的命令行应该是
frama-c test.c -rte -warn-unsigned-overflow -then -print -ocode <yourfile>
关于c - 带有Frama-c的RTE插件:无法识别“-rte-unsigned-ov”,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/57020749/