C99 promotion rules: what ?!

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.

1. blah blah "If both operands have the same type" nope
2. "if both operands have signed integer types or both have unsigned integer types" nope
3. "if the operand that has unsigned integer type has rank greater or equal to the rank of the type of the other operand" nope
4. "if the type of the operand with signed integer type can represent all of the values of the type of the operand with unsigned integer type" nope it's missing half of them.
5. "Otherwise both operands are converted to the unsigned integer type corresponding to the type of the operand with signed integer type."

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.