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.

Your question would be better if you showed a small example of C program and the result. As written, it can only be understood by people who already know Frama-C very well. If you provided an example, everyone could understand what your question is about. — Pascal Cuoq

Pascal Cuoq Pascal Cuoq · Accepted Answer · 2012-10-30T23:03:01

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

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

1 Answers