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.
$ 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.