Frama-c:将插件分析结果保存到c文件中

Question

我是frama-c的新手。所以我为我的问题提前道歉。

我想做一个插件，它将修改源代码，克隆一些函数，插入一些函数调用，我希望我的插件生成第二个文件，其中将包含输入文件的修改版本。

我想知道是否可以使用frama-c生成一个新的文件c。例如，Sparecode和语义常量折叠插件的结果直接显示在终端上，而不是以文件形式显示。所以我想知道Frama-c是否具有写入文件的功能，而不是将分析结果发送到标准输出。

当然，我们可以将frama-c的输出重定向到file.c。例如，在本例中，对于插件scf，value的结果在那里，我发现frama-c用while替换了例如" for“循环。

但我希望的是，frama-c可以生成一个文件，该文件将包含我的原始代码加上我想要插入的修改。

我查看了src / kernel_services / ast_printing目录，但没有真正找到可以指导我的函数。

谢谢。

Answer 1

在命令行上，选项-ocode <file>表示任何后续的-print都将在<file>中完成，而不是标准输出(如果您想再次在标准输出上打印，请在这之后使用-ocode "" )。请注意，-print会打印与当前项目对应的代码。您可以使用-then-on <prj>更改您感兴趣的项目。当然，更多信息可以在the user manual上找到。

当然，所有这些都可以通过编程实现。特别是，默认情况下，File.pretty_ast会在标准输出上打印(即输出C程序)当前项目的AST，但是有两个可选参数用于更改项目或输出应该使用的格式化程序。