作为独立的CBMC？

Question

作为独立的Visual运行CBMC是否可能？我是否需要重新编译它，还是还有其他的窍门？

我只需要经常使用CBMC将函数转换为CNF，所以我想用函数名调用它，将cnf文件写入磁盘，然后重新启动。我不想使用。

Answer 1

将CBMC模型检验器作为独立程序运行是完全可能的。我每周在Linux和Windows 7上做一次)

我假设您在Windows上是因为Visual的缘故。

打开一个命令提示符，导航到cbmc.exe所在的文件夹，然后按如下方式调用它：cbmc --help ...to，查看您所拥有的选项。

用户手册在3.2 Command line interface中有一节介绍了如何做到这一点。您可能必须调用为CLI设置Visual环境的批处理脚本(VSVARS32.bat / vsvarsall.bat等)。在某些Windows机器上，如果我没有记错的话，这个脚本就会放在c:\program files\microsoft visual studio\[version]\vc\bin\中。

有关：https://msdn.microsoft.com/en-us/library/f2ccy3wt.aspx的更多信息，请参见此MSDN页面。