是否可以将代码转换的结果写回原始源文件？
Is it possible to write the result of code transformations back to the original source files?
我想对 多个 文件执行代码转换，并将这些转换产生的更改写回原文件，最好是原始文件。例如，我想向源自文件 fileA.c 的函数 funcA 和文件 fileB.c 中定义的函数 funcB 添加一个 if 语句。在 funcA 和 funcB 上执行转换后，我想用生成的源代码覆盖文件 fileA.c 和 fileB.c。我不一定需要宏扩展之前的源代码（我怀疑这是不可能的）。
是否有使用 Frama-C 执行此操作的明智方法？
目前，您可以通过简单地将输出写入文件（使用选项 -print 和 -ocode <file>）对单个文件执行此操作，如在：
frama-c file.c [add your transformation options here] -print -ocode file.c
这会起作用，因为 Frama-C 读取输入源文件以解析它们并在实际写入输出之前构建其 AST。因此，当它截断原始文件以开始覆盖它时，文件已经被完全读取。
请注意，严格来说，此行为将来可能会改变（换句话说，这 不是 推荐的使用方式 Frama-C，尽管它应该在实践中工作）。
但是，对于多个文件，目前这是不可能的：Frama-C总是将它们全部合并为一个，统一的 AST，在进一步处理之前。虽然 AST 元素确实保留了有关它们来自哪个源文件的位置信息，但目前没有任何内容告诉 pretty-printer 将每个部分输出到不同的文件。
请注意，一般来说，这有点复杂：C 允许多次声明全局变量，因此您可以有一个文件 a.c 声明一个 struct st; 而不指定其字段，然后另一个文件 b.c 实际上声明了它的字段；当 pretty-printing 这些文件时，您需要记住所有原始声明。根据所执行的语法更改的类型，这些可能会影响某些声明，但不会影响全部。
总的来说，我认为理论上 可能 以某种方式告诉 Frama-C 记住所有这些细节并尝试使用位置信息来 pretty-print 它的AST 到多个文件（如果我们包括逻辑预处理，带有 ACSL 注释等，我什至不确定这是否可行），但它需要对内核进行 deep 更改。
因此，目前我认为没有明智的方法告诉 Frama-C 去做，至少在一般情况下是这样。对于一些与之相关的特定子任务（例如，pretty-printing 一些 select 全局变量），可以创建一个 AST 访问者，当访问这些元素时，pretty-print 将它们保存到一个文件中其名称与原始名称相关（例如，对于位置为 f.c 的 AST 节点，将其打印为 f-out.c）。但是确保这些文件在 all 情况下在语法上是有效的 C 会使它变得更加复杂。并且至少需要为脚本编写相当数量的 OCaml 代码。
我想对 多个 文件执行代码转换，并将这些转换产生的更改写回原文件，最好是原始文件。例如，我想向源自文件 fileA.c 的函数 funcA 和文件 fileB.c 中定义的函数 funcB 添加一个 if 语句。在 funcA 和 funcB 上执行转换后，我想用生成的源代码覆盖文件 fileA.c 和 fileB.c。我不一定需要宏扩展之前的源代码（我怀疑这是不可能的）。
是否有使用 Frama-C 执行此操作的明智方法？
目前，您可以通过简单地将输出写入文件（使用选项 -print 和 -ocode <file>）对单个文件执行此操作，如在：
frama-c file.c [add your transformation options here] -print -ocode file.c
这会起作用，因为 Frama-C 读取输入源文件以解析它们并在实际写入输出之前构建其 AST。因此，当它截断原始文件以开始覆盖它时，文件已经被完全读取。
请注意，严格来说，此行为将来可能会改变（换句话说，这 不是 推荐的使用方式 Frama-C，尽管它应该在实践中工作）。
但是，对于多个文件，目前这是不可能的：Frama-C总是将它们全部合并为一个，统一的 AST，在进一步处理之前。虽然 AST 元素确实保留了有关它们来自哪个源文件的位置信息，但目前没有任何内容告诉 pretty-printer 将每个部分输出到不同的文件。
请注意，一般来说，这有点复杂：C 允许多次声明全局变量，因此您可以有一个文件 a.c 声明一个 struct st; 而不指定其字段，然后另一个文件 b.c 实际上声明了它的字段；当 pretty-printing 这些文件时，您需要记住所有原始声明。根据所执行的语法更改的类型，这些可能会影响某些声明，但不会影响全部。
总的来说，我认为理论上 可能 以某种方式告诉 Frama-C 记住所有这些细节并尝试使用位置信息来 pretty-print 它的AST 到多个文件（如果我们包括逻辑预处理，带有 ACSL 注释等，我什至不确定这是否可行），但它需要对内核进行 deep 更改。
因此，目前我认为没有明智的方法告诉 Frama-C 去做，至少在一般情况下是这样。对于一些与之相关的特定子任务（例如，pretty-printing 一些 select 全局变量），可以创建一个 AST 访问者，当访问这些元素时，pretty-print 将它们保存到一个文件中其名称与原始名称相关（例如，对于位置为 f.c 的 AST 节点，将其打印为 f-out.c）。但是确保这些文件在 all 情况下在语法上是有效的 C 会使它变得更加复杂。并且至少需要为脚本编写相当数量的 OCaml 代码。