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

Since CBMC can produce a significant amount of output your best bet would be to work out how to call if from the command line.

Once you have done that then you can use the subprocess.call library function to call the same with the output redirected to a file, then process the contents of the file.

I would suggest using the --xml-ui flag to tell CBMC that you would like machine processable output.

Answer 2

CBMC can also produce JSON output using --json-ui since version 5.5, which is more compact than the XML output. Also note that you can suppress certain messages by adjusting the verbosity level using --verbosity <some number between 0 and 10>.