CBMC作爲獨立？

是否可以獨立運行CBMC作爲獨立的Visual Express？我是否需要重新編譯它或者是否還有其他技巧？CBMC作爲獨立？

我只需要使用CBMC定期將函數轉換爲CNF，所以我想用函數名稱來調用它，將cnf文件寫入磁盤並重新啓動。我不想使用Visual Studio。

2014-11-15 Adrian Monk

完全可以將The CBMC model checker作爲獨立程序運行。我在Linux和Windows 7上每週都會這樣做:)

我假設你在Windows上是因爲Visual Studio。

打開命令提示符並導航到cbmc.exe所在的文件夾，並按如下所示調用它：cbmc --help ...查看您擁有的選項。

user manual有一個關於如何去做的部分，在3.2 Command line interface。您可能需要調用爲CLI設置Visual Studio環境的批處理腳本（VSVARS32.bat/vsvarsall.bat等）。在某些Windows機器上，如果我記得正確，該腳本將被放置在c:\program files\microsoft visual studio\[version]\vc\bin\中。

上獲取更多信息，請參閱此MSDN頁：https://msdn.microsoft.com/en-us/library/f2ccy3wt.aspx

來源

2015-04-15 20:50:05

非常感謝你。那是我尋找的答案。 –

@AdrianMonk沒問題:)如果遇到問題，請查看手冊，或者進一步編輯問題。如果一切都適合你，請隨時上傳和/或接受我的答案。 –

Tusen Takk。我想製作cnf文件，但之後需要進行分區以便更好地計算。你也有這個工作嗎？也許Metis？我有一個問題需要將cnf文件導入Metis。 –

CBMC作爲獨立？

回答

相關問題