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] adjacent_find problem

Hello,

> thanks for your answer but I do not see where an overflow could occur.

Technically, Guillaume did not say there could be an overflow
in an expression inside your predicates. He said you wrote
some of them using "possibly overflowing [int] arithmetic".

By typing your predicate as accepting an int, you forced a
cast to be applied to its argument each time the argument is
of type integer. This is what Jessie is warning you about.
ints can be promoted to integers silently, but the conversion
in the other direction involves loss of information and
requires an explicit "(int)" cast.

One last word: it's the ACSL type-checker talking here, not any prover.
The type-checker is simple-minded and does not know that there
cannot be an overflow in the conditions you are in. From this
point of view it is just like the type-checker of any 
programming language.

Regards,

Pascal