--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on March 2012 ---
Hello Boris, 2012/3/12 Boris Hollas <hollas at informatik.htw-dresden.de>: > I want to substitute variables with pointer expressions, for example x > -> *p in x >= 0, where x and *p are given as logic_var. I'm not sure I'm following you here: by definition *p is not a logic_var. Do you mean that you have x and p, with p having pointer type and needing possibly several dereferences in order to obtain a value of the same type as x? > > 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 Again, I don't understand: TVar lv has type lv.lv_type, regardless of the fact that this type is an integral type or a pointer. > 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. No, this would not be correctly typed. The representation of *p as term_lhost is TMem (Logic_const.tvar lv). This term_lhost itself has type Logic_utils.typ_to_logic_type (Cil.typeOf_pointed (Logic_utils.logicCType lv.lv_type))) i.e. we remove one level of pointer. If p has type int**, TMem don't magically gives back an int. > > 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 Yes, this is the only sensible solution here: if you have several levels of pointers and want to get an int, you have to add several levels of TMem. And indeed, there's no function in the kernel to do that. > tree. Note that Logic_const.tvar doesn't add a TMem if lv has pointer > type. Why would tvar do that? It is a constructor. It does not try to build an integral value from an arbitrary variable lv (in fact that does not have any sense in the general case). Its purposes is only to build the term corresponding to lv i.e. term_node = TLval(Tvar lv, TNoOffset); term_type=lv.lv_type Best regards, -- E tutto per oggi, a la prossima volta Virgile