python - CBMC call from Python?

Question

Is there a way that I can call CBMC from Python or is there any wrapper or API for it available?

My Problem is the following. I want to create a C function automatically in Python (this works quite well) and sent them to CBMC from Python for checking and get feedback if the function is OK or not.

Answer 1

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

完成后，您可以使用subprocess.call 库函数调用相同的输出重定向到文件，然后处理文件的内容。

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

Answer 2

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