--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2012 ---
Hello Boris, 2012/8/2 Boris Hollas <hollas at informatik.htw-dresden.de>: > I have the following problem: I hash a term, but I can't find it later in > the hashtable. I was able to narrow the problem down to the following: > > In an assignment > int t = ...; > the lval t has type int, whereas an expression > t-1 > has type integer. To construct a term of t, I use the function term_of_lval > below. This should produce a term of type integer, but it doesn't. Instead, > the result is a term of type int. Since the cast flag in > Logic_utils.lval_to_term_lval is false, I'd have expected that int is cast > to integer. What is wrong here? > I'm not sure how this is related to your hashing issue, but the point here is that t has indeed int type. It gets _converted_ in an integer value whenever this is needed (in particular when t is used as an operand for an arithmetic operator, or passed to a function expecting an integer), but the lval itself keeps its int type. If you want to produce directly a term that has integer type, use let t = Logic_const.term (TLval xtl) Cil_types.Linteger in (of course, xtl must have an integral type for this to make sense). Best regards, -- E tutto per oggi, a la prossima volta Virgile