--- layout: post author: Pascal Cuoq date: 2011-04-11 15:05 +0200 categories: CIL conversions-and-promotions rant format: xhtml title: "C99 promotion rules: what ?!" summary: --- {% raw %}
I reported bug 785 after getting three-quarters sure that the problem was in Frama-C (I used two different versions of GCC as oracles).
I still cannot believe how twisted integer promotion rules are in C99. I had read them before but I had not followed the precise path I followed today in the various cases of 6.3.1.8.
The fun starts earlier in 6.3.1.3 with the definition of conversion rank.
rank(long long int) > rank(long int) even when these two types have the same size. But:
The rank of any standard integer type shall be greater than the rank of any extended integer type with the same width.
So if a compiler defines an extended long long long
type programs that use them will become differently typed the day long long long
becomes a standard type. Until it is standardized it has lower rank than a standardized type of the same size. When it becomes standardized it will probably get a higher rank than other standardized types of the same size.
Well never mind this: it is unclear whether this can have any effect on the computations in practice (it matters only when types have exactly the same size). Let's see what in 6.3.1.8 applies to bug 785 starting with the promotions applicable to 0x090E7AF82577C8A6LL | x9[1][0]
.
We have a `long long` on the left-hand side an `unsigned long` on the right-hand side. Oh and in this platform description `long` and `long long` are both the same size 64-bit.
There is a philosophy hidden in there. The philosophy seems to be "favor unsigned types unless the signed type makes more sense". Even a signed type of higher hank may see its values converted to the unsigned version of the same type changing the meaning of half of them. The rank matters only when it confirms that the unsigned type should be favored. You may be forgiven for wondering why we bother with ranks at all.
In conclusion both 0x090E7AF82577C8A6LL
and x9[1][0]
should be promoted to unsigned long long
which shall also be the type of the result. This is not what Carbon does.