Skip to content

Incorrect integer promotion for bit-fields #212

@jprotopopov-ut

Description

@jprotopopov-ut

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions