【发布时间】：2016-07-22 02:50:03
【问题描述】：
是否可以在没有 Visual Express 的情况下独立运行 CBMC？我需要重新编译它还是 可能还有什么技巧？
我只需要定期使用 CBMC 将一个函数转换为 CNF，所以我想调用它 函数名，将cnf文件写入磁盘并重新启动。我不想使用 Visual Studio。
【问题讨论】：
标签： c visual-studio cbmc
【发布时间】：2016-07-22 02:50:03
【问题描述】：
完全可以将The CBMC model checker 作为独立程序运行。 我每周在 Linux 和 Windows 7 上执行一次 :)
由于 Visual Studio，我假设您使用的是 Windows。
打开命令提示符并导航到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
【讨论】：
-
非常感谢。这就是我一直在寻找的答案。
-
@AdrianMonk 没问题 :) 如果您遇到困难，请查看手册，或者如果您遇到问题，请进一步编辑您的问题。如果一切都适合您，请随时投票和/或接受我的回答。
-
图森塔克。我想制作cnf文件，但之后需要分区以便更好地计算。你也在这方面工作吗？也许梅蒂斯？我在将 cnf 文件导入 Metis 时遇到问题。
-
@AdrianMonk Selv tak :) 不，我没有尝试从 SMT 后端导出定理/谓词，但我认为应该可以。我不确定如何以 CNF 形式获取它们，但如果输出是 SMT-lib 格式，也许还有其他工具可以。我已经看到你关于这个的其他问题，但我不能帮助你。我可以问一下这个应用程序是什么吗？