--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on January 2010 ---
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