--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on August 2012 ---
2012/8/2 Boris Hollas <hollas at informatik.htw-dresden.de>: > Hello Virgile, > > the problem is that if I hash t as an int (converted from an lval) and then > try to find t, when it is part of another term such as t-1, in the > hashtable, it has type integer and hence isn't found. 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) > > So, does "If cast is true: expressions with integral type are cast to > corresponding C type." in the API doc for expr_to_term, lval_to_term_lval, > host_to_term_host mean that the operand keeps type int, but is considered as > an integer when needed? t has always type int. When ~cast is true, casts are inserted over the result of arithmetic operations, in order to force the ACSL expression to have the same value as the C one (assuming 2-complement arithmetic for signed integral types). Otherwise, the result will be an unbounded integer. -- E tutto per oggi, a la prossima volta Virgile