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: virgile.prevosto at m4x.org (Virgile Prevosto)
- Date: Thu, 15 Mar 2012 09:56:38 +0100
- In-reply-to: <1331537104.6161.846.camel@iti27.informatik.htw-dresden.de>
- References: <1330091763.2071.50.camel@iti27.informatik.htw-dresden.de> <CA+yPOVgMt=gL_ta6EybZdxEdueW+-S0UMOgfXND8EH90VUF_GA@mail.gmail.com> <1331537104.6161.846.camel@iti27.informatik.htw-dresden.de>
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
- Follow-Ups:
- [Frama-c-discuss] Substitution in Cil_types.predicate
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Substitution in Cil_types.predicate
- References:
- [Frama-c-discuss] Substitution in Cil_types.predicate
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Substitution in Cil_types.predicate
- Prev by Date: [Frama-c-discuss] Substitution in Cil_types.predicate
- Next by Date: [Frama-c-discuss] Modifying the AST to insert statements / declarations
- Previous by thread: [Frama-c-discuss] Substitution in Cil_types.predicate
- Next by thread: [Frama-c-discuss] Substitution in Cil_types.predicate
- Index(es):