c - Frama-C: Replacing a Cil Term in a Cil Predicate

Question

Using the Cil_datatypes module defined in the Frama-C API, I am trying to replace a term (Cil_datatype) with a new term in a predicate (Cil_datatype). To do that I need to map a predicate with a function that when it finds the term (or terms) replaces it there. How do you map over a predicate to replace a term?

Answer 1

I think that you are looking for the visitor mechanism described in section 4.16 of the plugin development guide. Basically, you inherit from the Visitor.frama_c_copy or Visitor.frama_c_inplace class and redefines the vterm method so that it returns the modified term where needed. To initiate the visit, you then can call Visitor.visitFramacIdPredicate (or a similar function depending on the exact type of the predicate) with an instance of your class and the predicate to modify.

Note that if you do in-place modifications, your transformations might interfere with the annotation management done by the Frama-C kernel. It is thus better let Visitor.frama_c_copy perform a deep copy of the predicate.