Compiling code using initializer with possibly invalid constant expression about compcert HOT 2 CLOSED

This is one aspect where CompCert sticks to the ISO C standard.

A pointer value with static pointer type can be "casted" to a large enough integer type, but any arithmetic operation over the resulting pointer value with integer type is undefined. The only safe operation that can be done over such a value is casting it back to a pointer type. You can check this aspect of the CompCert C formal semantics using the reference interpreter (ccomp -interp).

Evaluation of compile-time constant expressions, in global initializers and elsewhere, is done essentially like the reference interpreter, following the formal semantics. Hence, the initializer above is reported as a compile-time error, because it corresponds to undefined run-time behavior.

GCC and Clang are more lenient, probably because they have an execution model in mind that is more lenient than the ISO C standard concerning arithmetic on pointer values having static integer type. I don't think CompCert can go this way, though, because it would break abstraction properties of pointer values that are necessary for correct compilation.

from compcert.

Thank you very much for the explanation.

Indeed, in the original code, such operations seem reasonable for GCC/Clang because they reference offsets inside array variables, e.g.:

unsigned long a[10];
unsigned long b = {(unsigned long)a+1}; // or +3, +5, +7...

It seems such accesses are voluntarily misaligned, but always inside the bounds of the array, so in practice there is no overflow here, but it deviates from the standard nevertheless.

from compcert.