--- layout: fc_discuss_archives title: Message 104 from Frama-C-discuss on February 2012 ---
On Fri, 2012-02-24 at 15:47 +0100, Virgile Prevosto wrote: > Hello Boris, > > 2012/2/24 Boris Hollas <hollas at informatik.htw-dresden.de>: > > I want to perform a substitution in a Cil_types.predicate, for example > > x->a in (0 <= x <= n). Is there a function in the Frama-C API to do so? > > There's nothing built-in, but a tiny copy visitor should do the trick. This works in a small example: method vterm t = begin match t.term_node with | TLval(TVar lv, offs) when Logic_utils.is_same_var lv lv_old -> let t_new = Logic_const.term (TLval(TVar lv_new, offs)) t.term_type in Cil.ChangeDoChildrenPost (t, fun _ -> t_new) However, I use the term_offset of t in t_new. Is this correct in general? With ChangeDoChildrenPost, it want to replace t with t_new. In 5.14.3., the meaning of ChangeDoChildrenPost is explained as follows: "ChangeDoChildrenPost(v,f) the old node is replaced by v, the visit goes on with the children of v, and when it is finished, f is applied to the result." - does "old node" mean the original node? - what does the "result" refer to? If it is the result of the visit, what is this? -- Best regards, Boris