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

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