[Frama-c-discuss] integer overflow
regehr at cs.utah.edu
Thu Jun 11 21:35:24 CEST 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
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?
More information about the Frama-c-discuss