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 18:46 +0100, Virgile Prevosto wrote:
> 2012/2/27 Boris Hollas <hollas at informatik.htw-dresden.de>:
> >
> > 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?
> 
> I'm not sure I understand exactly what you mean here. The behavior of
> the generic visitor is to visit each node in order, so basically yes,
> all logic_var below the starting point of the visit will be visited.

For example, a term_offset can be a TField of fieldinfo * term_offset.
fieldinfo contains fcomp : compinfo, which is the host structure of the
field. compinfo contains cname : string and ckey : int. Therefore, I
assume that the latter fields are not changed by method vlogic_var_use,
but they refer to the term_lhost part of term_lval = term_lhost *
term_offset. And a predicate may contain a term, which may have
term_lhost, term_offset as children. Hence, it is possible that
substituting only the logic vars (which may be contained in term_lhost)
results in terms that contain a reference to the old host?
-- 
Best regards,
Boris