--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on August 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Bug in Cil.datatype.Lval.Hashtbl?



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