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] integer overflow

  • Subject: [Frama-c-discuss] integer overflow
  • From: regehr at cs.utah.edu (John Regehr)
  • Date: Thu, 11 Jun 2009 13:35:24 -0600
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