--- layout: post author: Pascal Cuoq date: 2011-07-26 10:55 +0200 categories: conversions-and-promotions facetious-colleagues value format: xhtml title: "Fun with usual arithmetic conversions" summary: --- {% raw %}
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.