CBMC звонить с Python?
Есть ли способ, которым я могу вызвать CBMC из Python или есть какая-нибудь обертка или API для него?
Моя проблема заключается в следующем. Я хочу создать функцию C автоматически в Python (это работает довольно хорошо) и отправил их в CBMC из Python для проверки и получения обратной связи, если функция в порядке или нет.
2 ответа
Так как CBMC может производить значительный объем выходных данных, лучше всего было бы решить, как звонить из командной строки.
Как только вы это сделали, вы можете использовать subprocess.call библиотечная функция для вызова того же самого с выходом, перенаправленным в файл, а затем обработать содержимое файла.
Я бы предложил использовать --xml-ui флаг, указывающий CBMC, что вы хотите обработать машинный вывод.
CBMC также может производить вывод в формате JSON, используя --json-ui начиная с версии 5.5, которая более компактна, чем вывод XML. Также обратите внимание, что вы можете подавить некоторые сообщения, регулируя уровень детализации с помощью --verbosity <some number between 0 and 10>,