--- layout: fc_discuss_archives title: Message 8 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



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