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

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