--- layout: fc_discuss_archives title: Message 107 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Substitution in Cil_types.predicate



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