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语句，你可能需要自己写。