--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on March 2012 ---
Hello Virgile, > 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? yes > 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. Ok. Thanks for pointing this out! It might have been possible that someone has already done it. > 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. I agree if the meaning of the Logic_const.tX functions is "make a term that is an X". Without further documentation, tvar lv could also be understood as "make a term that corresponds to lv and represents lv.lv_type" (ie, Cil.d_term (tvar lv) would pretty print *p for a logic_var p of type int*). I know now that this notion is wrong. -- Best regards, Boris