--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on August 2012 ---
Hello, 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. This is invoked on each of two occurences of lval this->gear of type int that occurs twice in a c-file: module TermHT = Hashtbl.Make(struct type t = Cil_types.term let equal = Logic_utils.is_same_term let hash = Logic_utils.hash_term end) let debug_ht x = Self.feedback "Processing %a\n" Cil.d_lval x; if Cil_datatype.Lval.Hashtbl.mem lval_debug_ht x then Self.feedback "Lval %a already hashed!\n" Cil.d_lval x else Cil_datatype.Lval.Hashtbl.add lval_debug_ht x true; let xt = term_of_lval x in if TermHT.mem term_debug_ht xt then Self.feedback "Term %a already hashed!\n" Cil.d_term xt else TermHT.add term_debug_ht xt true I get "Term this->gear already hashed!" for the second occurence of this->gear, but not "Lval this->gear already hashed!". -Boris