Frama-C:替换Cil谓词中的Cil项
Frama-C:替换Cil谓词中的Cil项
提问于 2014-07-15 18:13:26
使用Frama中定义的Cil_datatypes模块，我试图将一个术语(Cil_datatype)替换为谓词(Cil_datatype)中的一个新术语。要做到这一点，我需要用一个函数映射一个谓词，当它找到该术语(或多个术语)时，它就会在那里替换它。如何映射谓词来替换一个术语？
回答 1
Stack Overflow用户
回答已采纳
发布于 2014-07-16 07:51:29
我认为您正在寻找the plugin development guide第4.16节中描述的访问机制。基本上，您继承了Visitor.frama_c_copy或Visitor.frama_c_inplace类，并重新定义了vterm方法，以便它在需要时返回修改过的术语。要启动访问，您可以使用类的实例和要修改的谓词调用Visitor.visitFramacIdPredicate (或类似的函数，具体取决于谓词的确切类型)。
注意，如果您进行就地修改，您的转换可能会干扰Frama内核所做的注释管理。因此，最好让Visitor.frama_c_copy执行谓词的深拷贝。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/24765286
复制相关文章
相似问题
腾讯云开发者
