从Python调用CBMC？

Question

有没有一种方法可以从Python调用CBMC，或者有没有可用的包装器或API？

我的问题如下。我想在Python中自动创建一个C函数(这工作得很好)，并将它们从Python发送到CBMC进行检查，并获得函数是否正常的反馈。

Answer 1

由于CBMC可以产生大量的输出，因此最好的办法是弄清楚如何从命令行调用if。

完成此操作后，您可以使用subprocess.call library function调用相同的方法，将输出重定向到一个文件，然后处理该文件的内容。

我建议使用--xml-ui标志来告诉CBMC您想要机器可处理的输出。

Answer 2

从版本5.5开始，CBMC还可以使用--json-ui生成JSON输出，它比XML输出更紧凑。还要注意的是，您可以通过使用--verbosity <some number between 0 and 10>调整详细级别来抑制某些消息。