--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on March 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Substitution in Cil_types.predicate



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