[Frama-c-discuss] integer overflow

[John Regehr]

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