c - Frama-C:替换 Cil 谓词中的 Cil 术语

Question

使用 Frama-C API 中定义的 Cil_datatypes 模块，我尝试用谓词 (Cil_datatype) 中的新术语替换术语 (Cil_datatype)。为此，我需要使用一个函数映射一个谓词，当它找到一个或多个术语时，它会在那里替换它。如何映射谓词来替换术语？

Answer 1

我认为您正在寻找the plugin development guide第4.16节中描述的访问者机制。基本上，您可以继承 Visitor.frama_c_copy 或 Visitor.frama_c_inplace 类，并重新定义 vterm 方法，以便它在需要时返回修改后的术语。要启动访问，您可以使用类的实例和要修改的谓词调用 Visitor.visitFramacIdPredicate(或类似的函数，具体取决于谓词的确切类型)。

请注意，如果您进行就地修改，您的转换可能会干扰 Frama-C 内核完成的注释管理。因此，最好让 Visitor.frama_c_copy 执行谓词的深层复制。