Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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