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

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