2

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 をコンパイルしました。

4

1 に答える 1

5 
$ 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ステートメントとラベルをこれらのターゲットとして、オプションではない方法で、たとえば||and などの他の構成要素の翻訳として導入します&&。この治療法を無効にする方法はありません。スライシング プラグインは AST の一部を選択し、他の部分を消去するため、gotoステートメントが出力に表示されます。

Frama-C のスライシング プラグインは、C プログラム用にコンパイル可能なスライスを生成する、私が知っている唯一のスライサーです。gotoステートメントを導入しないより優れたスライサーが必要な場合は、独自のスライサーを作成する必要がある場合があります。

于 2012-10-30T23:03:01.980 に答える