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: Tue, 07 Aug 2012 09:30:46 +0200
  • In-reply-to: <CA+yPOVjfUxxnMvroF0OJv18kX8H6Yv48mdQ4-JG=D-1f_6iVWA@mail.gmail.com>
  • References: <501F9E92.9060709@informatik.htw-dresden.de> <CA+yPOVjfUxxnMvroF0OJv18kX8H6Yv48mdQ4-JG=D-1f_6iVWA@mail.gmail.com>
Hello Virgile,

> As a matter of fact, this is a feature of Cil_datatype.Lval (more
> precisely Cil_datatype.Exp). As explained in the API for
> Cil_datatype.Exp and Cil_datatype.Lval,  hash and equality over C
> expressions use the eid field, which by construction will differ
> between two semantically equivalent but physically different
> expressions. As mentioned in the documentation, a more semantic notion

I read the line "Note that the equality is based on eid (for 
sub-expressions).", but I didn't tell me much. Does eid refer to 
Cil_types.exp.eid? If so, what happens if the lhost is a varinfo (which 
doesn't have a field eid)?

My code basically is

if(cond) this->gear++;
else this->gear--;

I don't see why this->gear should be considered being different here and 
I don't yet understand why I get different hash values. At least, this 
is utterly unexpected.

-Boris