frama-c - 是否可以将代码转换的结果写回原始源文件？

Question

我想对多个 文件执行代码转换，并将这些转换产生的更改写回原文件，最好是原始文件。例如，我想向源自文件 fileA.c 的函数 funcA 和函数 funcB 添加一个 if 语句在文件 fileB.c 中定义。在对 funcA 和 funcB 执行转换后，我想覆盖文件 fileA.c 和 fileB.c结果源代码。我不一定需要宏扩展之前的源代码(我怀疑这是不可能的)。

是否有使用 Frama-C 执行此操作的明智方法？

Answer 1

目前，您可以通过简单地将输出写入文件(使用选项 -print 和 -ocode <file> )来针对单个文件，如:

frama-c file.c [add your transformation options here] -print -ocode file.c

这是可行的，因为 Frama-C 读取输入源文件以解析它们并在实际写入输出之前构建其 AST。因此，当它截断原始文件以开始覆盖它时，该文件已经被完全读取。

请注意，严格来说，此行为将来可能会发生变化(换句话说，这不是使用 Frama-C 的推荐方式，尽管它在实践中应该有效)。 p>

但是，对于多个文件，目前这是不可能的:在进一步处理之前，Frama-C 总是将它们全部合并到一个统一的 AST 中。虽然 AST 元素确实保留了有关它们来自哪个源文件的位置信息，但目前没有任何信息告诉 pretty-print 将每个部分输出到不同的文件。

请注意，一般来说，这有点复杂:C 允许多次声明全局变量，因此您可以拥有一个文件 a.c声明 struct st;不指定其字段，然后是另一个文件 b.c它实际上声明了它的字段； pretty-print 这些文件时，您需要记住所有原始声明。根据所执行的语法更改的类型，这些可能会影响某些声明，但不会影响全部。

总的来说，我相信理论上可能以某种方式告诉 Frama-C 记住所有这些细节并尝试使用位置信息将其 AST 漂亮地打印到多个文件(如果我们包括逻辑预处理，使用 ACSL 注释等，我什至不确定这是否可行)，但它需要对内核进行深度更改。

因此，目前，我认为没有明智的方式告诉 Frama-C 这样做，至少在一般情况下是这样。对于一些与之相关的特定子任务(例如，漂亮地打印一些选定的全局变量)，可以创建一个 AST 访问者，当访问这些元素时，将它们漂亮地打印到一个名称与原始名称相关的文件中(例如，对于位置为 f.c 的 AST 节点，将其打印为 f-out.c )。但是确保这些文件在所有 情况下在语法上都是有效的 C 会使它变得更加复杂。并且至少需要为脚本编写相当数量的 OCaml 代码。