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

  • Subject: [Frama-c-discuss] Substitution in Cil_types.predicate
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Mon, 5 Mar 2012 19:10:59 +0100
  • In-reply-to: <1330428489.2127.89.camel@iti27.informatik.htw-dresden.de>
  • References: <1330091763.2071.50.camel@iti27.informatik.htw-dresden.de> <CA+yPOVgMt=gL_ta6EybZdxEdueW+-S0UMOgfXND8EH90VUF_GA@mail.gmail.com> <1330330506.2071.75.camel@iti27.informatik.htw-dresden.de> <CA+yPOVjC+ux_Rj+SwdLU4yOZeP2zcZvNFeSpD7698zqwx7BoSA@mail.gmail.com> <1330340425.2206.16.camel@iti27.informatik.htw-dresden.de> <CA+yPOVht1LJpDC3c+xq8fS6z+DjucQO5oTPrad5fr3+OzjejUA@mail.gmail.com> <1330353401.2206.29.camel@iti27.informatik.htw-dresden.de> <CA+yPOVjCm-h7_3+Vcww-Lqpk+j=ty_+P-3T=oFxbqd_YLb+ZQA@mail.gmail.com> <1330428489.2127.89.camel@iti27.informatik.htw-dresden.de>
2012/2/28 Boris Hollas <hollas at informatik.htw-dresden.de>:
> 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?

The generic visitor is meant to visit all the subnodes of the AST that
is given as root to the relevant visitFramac* function. Unless the
derived visitor explicitly stops the visit of some branch by using a
SkipChildren or ChangeTo(Post), all uses of logic_var below the root
of the visit will be visited (hence substituted if they match).

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile