--- layout: fc_discuss_archives title: Message 107 from Frama-C-discuss on February 2012 ---
2012/2/27 Boris Hollas <hollas at informatik.htw-dresden.de>: > >> or overload vlogic_var_use instead of vterm: >> method vlogic_var_use lv = >> ? if Logic_utils.is_same_var lv lv_old then Cil.ChangeTo lv_new else DoChildren > > but wouldn't this just replace the lv without substituting the > corresponding offset? No (NB: here lv is a logic_var, not an lvalue): the variable gets substituted when visiting the logic_var node. This has no influence over the visit of the offset, which is not a child of the logic_var node. > >> The latter can only be used for performing var-to-var substitution. > > if I want to substitute s->t in s.a and both s,t are vars of compatible > type, is this a var-to-var substitution? > Yes, what I meant was that you cannot substitute s by an arbitrary expression (e.g. t[3]) in this context, since you have to return a logic_var visitAction. >> Yes, old node means the original one, and the result is the result of >> visiting v. The result is whatever the visitor wants to do with the >> children of v. > > So the result is a visitAction? But fun _ -> t_new is applied on a term, > not on a visitAction. Or is the result the node of the corresponding > type after having been visited? > It is directly a term. Conversion from term visitAction to term is handled directly by the visitor mechanism. Note that for some methods (e.g. vstmt or vglob_aux), you may end up with a list of nodes instead of a unique node (allowing the visitor to easily add new statements or globals). Best regards, -- E tutto per oggi, a la prossima volta Virgile