--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on August 2012 ---
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