--- layout: fc_discuss_archives title: Message 111 from Frama-C-discuss on February 2012 ---
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