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?

Hello Boris,

2012/8/6 Boris Hollas <hollas at informatik.htw-dresden.de>:
> I have a problem similar to the one I reported last week, this time with
> lvals: I hash an lval and I'm unable to find it later. However, this problem
> vanishes if I convert this lval into a term using the functions in
> Logic_const and hash the resultant term.
>

I'd advise against translating to/from logic terms just for this
purpose, this might be a source of confusion, but it might be a
suitable workaround.
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
of equality can be obtained through Cil.compareLval, but there is no
associated comparison or hash function that would allow  to build maps
or hashtbl based on that. Feel free to add a feature request on the
BTS regarding that.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile