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