有没有一种方法可以从Python调用CBMC，或者有可用的包装器或API？
我的问题如下。我想在Python中自动创建一个C函数（效果很好），然后将它们从Python发送到CBMC进行检查，并在函数正常与否的情况下获取反馈。
最佳答案
由于CBMC可以产生大量输出，因此最好的选择是确定如何从命令行进行调用。
完成此操作后，可以使用subprocess.call library function调用相同的命令，并将输出重定向到文件，然后处理文件的内容。
我建议使用--xml-ui标志告诉CBMC您想要机器可处理的输出。