--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on August 2012 ---
Hello, 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? -Boris let term_of_lval x = Self.feedback "term_of_lval: input lval %a\n" Cil.d_lval x; let xtl = Logic_utils.lval_to_term_lval false x in let t = Logic_const.term (TLval xtl) (Cil.typeOfTermLval xtl) in Self.feedback "output has type %a\n" Cil.d_logic_type t.term_type; t