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-simplify-cfg 没有做任何事情，因为没有简化 break、continue 和 switch 语句已经是默认值了。

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

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