--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on August 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Bug in Cil.datatype.Lval.Hashtbl?



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