Frama-C选项-no-simplify-cfg不起作用

Question

我正在使用Frama-C来计算C程序的一部分.我希望切片程序看起来像没有代码转换的原始程序.但是在生成的切片中,我总是有goto语句和标签.我使用命令:

frama-c -no-simplify-cfg -main test -slice-assert test test.c -then-on 'Slicing export' -print -ocode result.c

我在Cygwin的Windows机器上从最新的Oxygen版本编译了Frama-C.

Answer 1

$ frama-c -kernel-help
[...]
-simplify-cfg   remove break, continue and switch statement[sic] before
                analyzes[sic] (opposite option is -no-simplify-cfg)

选项-no-简化-CFG没有做任何事情,因为不简化 break,continue并switch声明已经是默认的.

前端确实goto以非可选的方式将语句和标签作为目标引入,例如||和其他构造的翻译&&.没有办法禁用这种治疗方法.切片插件选择AST的一部分并擦除其他部分,因此goto语句出现在其输出中.

Frama-C的切片插件是我所知道的唯一能为C程序生成可编辑切片的切片器.如果你需要一个不会引入goto语句的更好的切片器,你可能需要自己编写.