Frama-c: сохранить результаты анализа плагина в файле c

Question

Я новичок в frama-c. Поэтому я заранее прошу прощения за мой вопрос.

Я хотел бы создать плагин, который будет изменять исходный код, клонировать некоторые функции, вставлять вызовы некоторых функций, и я хотел бы, чтобы мой плагин генерировал второй файл, который будет содержать измененную версию входного файла.

Я хотел бы знать, возможно ли создать новый файл c с frama-c. Например, результаты плагинов сворачивания Sparecode и Semantic отображаются непосредственно на терминале, а не в файле. Поэтому я хотел бы знать, есть ли у Frama-c функция записи в файл вместо отправки результата анализа в стандартный вывод.

Конечно, мы можем перенаправить вывод frama-c, например, в файл file.c, но в этом случае для плагина scf, например, результаты value есть, и я обнаружил, что frama-c заменяет, например, "for покажется

Но я хотел бы, чтобы frama-c мог генерировать файл, который будет содержать мой исходный код плюс изменения, которые я бы вставил.

Я посмотрел в каталоге src / kernel_services / ast_printing, но я действительно не нашел функций, которые могут мне помочь.

Благодарю.

Answer 1

В командной строке опция -ocode <file> указывает на то, что любой последующий -print будет сделано в <file> вместо стандартного вывода (используйте -ocode "" после этого, если вы хотите снова напечатать на стандартный вывод). Обратите внимание, что -print печатает код, соответствующий текущему проекту. Ты можешь использовать -then-on <prj> изменить проект, который вас интересует. Более подробная информация, конечно, доступна в руководстве пользователя.

Все это, конечно, доступно программно. Особенно, File.pretty_ast по умолчанию pretty-prints (т.е. вывод программы C) AST текущего проекта на stdout, но принимает два необязательных аргумента для изменения проекта или средства форматирования, в которые должен быть выполнен вывод.