小编use*_*344的帖子

我正在使用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.