python - Python からの CBMC 呼び出し?

Question

Python から CBMC を呼び出す方法はありますか、またはそのためのラッパーまたは API はありますか?

私の問題は次のとおりです。Python で C 関数を自動的に作成し (これは非常にうまく機能します)、それらを Python から CBMC に送信して、関数が正常かどうかを確認し、フィードバックを得たいと考えています。

Answer 1

CBMC は大量の出力を生成する可能性があるため、コマンド ラインから if を呼び出す方法を考えるのが最善の策です。

それが完了したら、subprocess.call ライブラリ関数を使用して、出力をファイルにリダイレクトして同じ関数を呼び出し、ファイルの内容を処理できます。

フラグを使用して、--xml-uiマシンで処理可能な出力が必要であることを CBMC に伝えることをお勧めします。