--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on June 2009 ---
On June 5 Pascal Cuoc said: > The value analysis *could* take care of that and emit an alarm > each time it can't ensure that no overflow occurs. Currently, > it assumes that all overflows are desired overflows that are part > of the program's logic, and it continues the analysis with a > correct superset of the values that can actually be obtained > at run-time, assuming 2's complement arithmetic and proper > configuration of the characteristics of the target architecture. This seems slightly worrisome. Just to be clear, of course C has different kinds of overflow: First, overflow of unsigned math operators is defined to have modulo behavior. Second, overflow in lossy integer casts (for example, casting int to short) is implementation defined. However, all common C compiler do the obvious thing. Third, overflow of signed arithmetic (for example, MAX_INT+1) is undefined. Due to C's semantics, the "correct superset of the values that can actually be obtained at run-time" does not exist. Rather, anything at all can happen including terminating with a signal, continuing to execute with a corrupt state, etc. A C program should never continue to execute after executing an operation with undefined behavior, and so it seems rather important for Frama-C to give rigorous warnings in this case. Optimizing C compilers including gcc routinely exploit the undefined nature of signed overflow! Anyway, I have some C functions for which I want to prove the absence of the third kind of overflow, which results in undefined behavior. Is there a way to get Frama-C to help me do this? Thanks, John Regehr