--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on August 2012 ---
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) I used Cil_datatype.Term.Hashtbl. Now I've replaced this with module TermHT = Hashtbl.Make(struct type t = Cil_types.term let equal = Logic_utils.is_same_term let hash = Logic_utils.hash_term end) and the problem has disappeared. The problem was: - For int x = ... I hashed term_of_lval x, converting x to type integer. - Later in ... = x-1 I could't find x in the hashtab, although it contained a term x of kind TLval and type integer. The pretty-printing functions and extensive debugging didn't give a clue as what the problem might be. How does Logic_utils.is_same_term differ from Cil_datatype.Term.equal and what should be used for the hashtable? -Boris