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

[Frama-c-discuss] Problem with int and integer in terms



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