Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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