Goblint version: nightly sha256:454ed1481fd6d78e45ed0e58e458f5a32312491f2552535b5cf18e2077447a2d.
When processed with --enable justcil, the following code snippet
struct X {
long x : 7;
} x;
struct Y {
long y : _Generic(x.x + 1, int : 1, default : -1);
};
produces
struct Y {
long y : -1 ;
};
which contradicts C23 language standard. In particular, section 6.3.1.1 specifies (first paragraph on page 47):
If the original type is not a bit-precise integer type (6.2.5): if an int can represent all
values of the original type (as restricted by the width, for a bit-field), the value is converted to an
int; otherwise, it is converted to an unsigned int. These are called the integer promotions. All
other types are unchanged by the integer promotions
In the example above, bit-field long : 8 is representable by int, and thus the value of x.x in the expression shall be promoted to int. This interpretation is consistent with behavior of clang and gcc. Goblint seems to promote based on the type alone, disregarding bit-field width.
Goblint version: nightly sha256:454ed1481fd6d78e45ed0e58e458f5a32312491f2552535b5cf18e2077447a2d.
When processed with
--enable justcil, the following code snippetproduces
which contradicts C23 language standard. In particular, section 6.3.1.1 specifies (first paragraph on page 47):
In the example above, bit-field
long : 8is representable byint, and thus the value ofx.xin the expression shall be promoted toint. This interpretation is consistent with behavior of clang and gcc. Goblint seems to promote based on the type alone, disregarding bit-field width.