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] 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