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] Bug in Cil.datatype.Lval.Hashtbl?

  • Subject: [Frama-c-discuss] Bug in Cil.datatype.Lval.Hashtbl?
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Thu, 09 Aug 2012 08:31:41 +0200
  • In-reply-to: <CABbVA-Ar12teAApmabt_2DHj=vkUML+ZJwxY47W8zXoZvkGFnQ@mail.gmail.com>
  • References: <501F9E92.9060709@informatik.htw-dresden.de> <CA+yPOVjfUxxnMvroF0OJv18kX8H6Yv48mdQ4-JG=D-1f_6iVWA@mail.gmail.com> <5020C426.501@informatik.htw-dresden.de> <CABbVA-Ar12teAApmabt_2DHj=vkUML+ZJwxY47W8zXoZvkGFnQ@mail.gmail.com>
Hello,

> As 'this' is a pointer, this->gear is represented internally as
>
> Mem ({ enode = Var vthis; ...}, Field (fgear, NoOffset))

I think it's
(Mem {enode = Lval(Var vthis, NoOffset); ....}, Field (fgear, NoOffset))


> The first argument of the Mem constructor is an expression. Thus, your
> two occurrences of this->gear will contain two different
> Cil_types.exp, that will have two different eids. The two lvals will

I understand that this->gear++, this->gear-- are different expressions. 
But why are the inner expressions this->gear different? How are the eids 
generated?

Are the respective vids equal?

> want is given by the functions Cil.compareExp and Cil.compareLval, but

These use ==. Is it possible to access the physical representation of ADTs?

- Boris