Frama-C option -no-simplify-cfg does not work

Question

I am using Frama-C to compute a slice of a C program. I want the sliced program to look like the original without code transformation. However in the resulting slice I always have goto statements and labels. I use the command:

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

I compiled Frama-C from the latest Oxygen release on a Windows machine under Cygwin.

Answer 1

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

Option -no-simplify-cfg does not do anything because not simplifying break, continue and switch statements is already the default.

The front-end does introduce goto statements and labels as targets for these in a non-optional fashion as the translation of other constructs, for instance || and &&. There is no way to disable this treatment. The slicing plug-in selects parts of the AST and erases others, therefore the goto statements appear in its output.

Frama-C's slicing plug-in is the only slicer I know that produces compilable slices for C programs. If you need a better slicer that does not introduce goto statements, you may need to write your own.