--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on August 2012 ---
Hello, 2012/8/2 Boris Hollas <hollas at informatik.htw-dresden.de>: > On 02.08.2012 15:01, Virgile Prevosto wrote: >> Which hash function are you using? You might want to try >> Logic_utils.hash_term for your purpose (in Nitrogen, >> Cil_datatype.Term.hash uses Hashtbl.hash, which gives different >> results on terms that are considered equal by Cil_datatype.Term.equal, >> which might be the cause of the issue you're seeing. This will be >> fixed in Oxygen) > > How does Logic_utils.is_same_term differ from Cil_datatype.Term.equal and > what should be used for the hashtable? > Basically, my suggestion above must be seen as a workaround for an issue with Cil_datatype.Term.hash in Nitrogen. When it will be fixed in Oxygen, you should use functions from Cil_datatype.Term. Logic_utils functions are meant to be used in very particular contexts. In fact, the main (and possibly only) use case is the merging phase at the end of elaboration when you have several source files and thus cannot rely on vid &al to tell if two identifiers are the same, and must switch to a comparison with the name of the identifier. Cil_datatype operates in context where all symbols have been merged, and thus use the relevant id field for that purpose. This is the case for almost all Frama-C's operation, and unless you have a very peculiar need (or there is a bug in Cil_datatype ;-), you should stick with that. Best regards, -- E tutto per oggi, a la prossima volta Virgile