Я использую Frama-C для вычисления фрагмента программы C. Я хочу, чтобы нарезанная программа выглядела как оригинал без преобразования кода. Однако в результирующем фрагменте у меня всегда есть операторы goto и метки. Я использую команду:
frama-c -no-simplify-cfg -main test -slice-assert test test.c -then-on 'Slicing export' -print -ocode result.c
Я скомпилировал Frama-C из последней версии Oxygen на машине с Windows под Cygwin.
$ 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 и switch уже заданы по умолчанию.
Внешний интерфейс вводит операторы goto и метки в качестве целей для них необязательным образом, как перевод других конструкций, например || и &&. Невозможно отключить это лечение. Подключаемый модуль нарезки выбирает части AST и стирает другие, поэтому в его выводе появляются операторы goto.
Модуль слайсера Frama-C — единственный известный мне слайсер, который создает компилируемые слайсы для программ на языке C. Если вам нужен лучший слайсер, который не вводит операторы goto, вам может понадобиться написать свой собственный.
