--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on March 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Substitution in Cil_types.predicate



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