c - スタンドアロンとしてのCBMC?

Question

Visual Express なしでスタンドアロンとして CBMC を実行することは可能ですか? 再コンパイルする必要がありますか、それとも別のトリックがありますか?

関数を CNF に定期的に変換するために CBMC を使用するだけでよいので、関数名で呼び出し、cnf ファイルをディスクに書き込んで、最初からやり直します。Visual Studio を使用したくありません。

Answer 1

CBMC モデル チェッカーをスタンドアロン プログラムとして実行することは完全に可能です。Linux と Windows 7 の両方で毎週行っています :)

Visual Studio のために Windows を使用していると仮定しています。

コマンド プロンプトを開き、あるフォルダーに移動し、次のcbmc.exeように呼び出しcbmc --helpます。

ユーザーマニュアルには、その方法に関するセクションがあります3.2 Command line interface。CLI 用に Visual Studio の環境をセットアップするバッチ スクリプト (VSVARS32.bat / vsvarsall.bat など) を呼び出す必要がある場合があります。c:\program files\microsoft visual studio\[version]\vc\bin\一部の Windows マシンでは、私の記憶が正しければ、そのスクリプトが配置されています。

詳細については、この MSDN ページを参照してください: https://msdn.microsoft.com/en-us/library/f2ccy3wt.aspx