--- layout: fc_discuss_archives title: Message 108 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



On Mon, 2012-02-27 at 14:31 +0100, Virgile Prevosto wrote:
> > 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.

But a term may have - via term_lval = term_lhost * term_offset - a
logic_var and an offset as children. Is the term_offset copied by the
default method of the copy visitor and references in offset to the old
base variable (eg s in s.a) - if any - are of type logic_var and thus
substituted by the visitor?


-- 
Best regards,
Boris