--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on March 2012 ---
Hello, I want to substitute variables with pointer expressions, for example x -> *p in x >= 0, where x and *p are given as logic_var. This doesn't work by substituting the corresponding logic_vars by overriding vterm or vlogic_var_use in a visitor. One solution is to build term-parts corresponding to the logic_vars and to substitute these by overriding vterm. Yet, I haven't found a function to build eg a term_lhost from a logic var lv that respects the Ctype of lv. For example, *p must be converted into TMem(Logic_const.term (TLval(TVar lv, TNoOffset)) (base_type lv.lv_type)) where lv is the vlogic_var_assoc of *p and base_type returns the base integral type. A solution to this may be to count the number of TPtrs in the Ctype of lv and add a corresponding number of TMems in the term_lhost syntax tree. Note that Logic_const.tvar doesn't add a TMem if lv has pointer type. However, I'm not sure if this is a good approach. -- Best regards, Boris