Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Bug in Cil.datatype.Lval.Hashtbl?
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Mon, 06 Aug 2012 12:38:10 +0200
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