1

frame-c Web サイトhttp://frama-c.com/download.htmlから Windows インストーラーの Boron バージョンをインストールしました。

val プラグインを実行しようとすると、プリプロセッサ変数 CPP が次のように設定されていないというエラーが表示されます。 

C:\Frama-C\bin>frama-c.exe -val filename.cpp
[kernel] user error: failed to run: gcc -C -E -I.  -o "C:\Users\akandoor\AppData\Local\Temp\filename.cpp4f5d23.i" "filename.cpp"
you may set the CPP environment variable to select the proper preprocessor command or use the option "-cpp-command".
[kernel] user error: skipping file "filename.cpp" that has errors.
[kernel] Frama-C aborted because of an invalid user input.

-cpp-command を使用すると、次のエラーが表示されます。 

C:\Frama-C\bin>frama-c.exe -cpp-command 'C:\utils\cygwin\bin\gcc.exe -C -E -I. -
x c' filename.cpp
[kernel] user error: option `-C' is unknown.
                     use `frama-c.exe -help' for more information.
[kernel] Frama-C aborted because of an invalid user input.

手がかり/提案はありますか？

4

1 に答える 1

1

ここに提案があります: 前処理が問題を引き起こしているので、前処理されたファイルを .i ファイルとして保存し、都合のよい方法で前処理を行ってください。次に Frama-C コマンドラインで .i ファイルを渡します。これにより、前処理を行う必要がないことがわかります。

注釈を .c ファイルに挿入する場合、または前処理オプションを変更する場合は、忘れずに .i ファイルを再生成してください。

最新の改善された Frama-C バージョンが必要な人に向けられることが多いもう 1 つの提案は、Linux 仮想マシン内にインストールすることです。これにより、すべてが機能します。デフォルトの PATH に GCC があり、この GCC はコマンドライン オプション-Cを使用し-Eて前処理します。Frama-C のほとんどのユーザーおよび開発者と同じ環境を使用することになります。また、より新しいバージョンを使用することもできます。

于 2014-03-12T21:22:33.140 に答える