Fun with usual arithmetic conversions

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.