--- layout: fc_discuss_archives title: Message 5 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,

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