use*_*590 2 c frama-c
使用Cil_datatypesFrama-C API中定义的模块,我试图用谓词(Cil_datatype)中的新术语替换术语(Cil_datatype).要做到这一点,我需要使用一个函数映射一个谓词,当它找到术语(或术语)替换它时.如何映射谓词来替换术语？
Cil_datatypes
Vir*_*ile 5
我认为您正在寻找插件开发指南第4.16节中描述的访问者机制.基本上,您从Visitor.frama_c_copyor或Visitor.frama_c_inplace类继承并重新定义vterm方法,以便在需要时返回修改后的术语.要启动访问,您可以Visitor.visitFramacIdPredicate使用类的实例和要修改的谓词来调用(或类似函数,具体取决于谓词的确切类型).
Visitor.frama_c_copy
Visitor.frama_c_inplace
vterm
Visitor.visitFramacIdPredicate
请注意,如果进行就地修改,则转换可能会干扰Frama-C内核完成的注释管理.因此,最好让我们Visitor.frama_c_copy执行谓词的深层复制.
归档时间：
11 年，6 月 前
查看次数：
72 次
最近记录：
11 年，5 月 前