Fun with usual arithmetic conversions

Pascal Cuoq - 26th Jul 2011

A facetious colleague reports the following program as a bug:

int main () { 
  signed char c=0; 
  while(1) c++; 
  return 0; 
} 

The commandline frama-c -val -val-signed-overflow-alarms charpp.c, he says, does not emit any alarm for the c++; instruction.

Indeed, the c++; above is equivalent to c = (signed char) ((int)c + 1);.

If the implementation-defined(6.3.1.3 §3) conversions from int to signed char are assumed to give the expected modulo results, this instruction never displays undefined behavior. The really dangerous operation, signed addition, takes place between arguments of type int and returns an int. Thus, in this particular program and for the default x86_32 target architecture, the result of the addition is always representable in the result type.

Pascal Cuoq
26th Jul 2011