frama-c - 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并且switchstatements 已经是默认设置。

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

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