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

  • Subject: [Frama-c-discuss] Substitution in Cil_types.predicate
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Mon, 12 Mar 2012 08:25:04 +0100
  • In-reply-to: <CA+yPOVgMt=gL_ta6EybZdxEdueW+-S0UMOgfXND8EH90VUF_GA@mail.gmail.com>
  • References: <1330091763.2071.50.camel@iti27.informatik.htw-dresden.de> <CA+yPOVgMt=gL_ta6EybZdxEdueW+-S0UMOgfXND8EH90VUF_GA@mail.gmail.com>
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