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