Unexpected verification result related to bit-field

[muchang]

struct X {
   unsigned long u31:31;
};

struct X x;

int main ()
{
      if ((x.u31 - 2) >= 0)
	{assert(0);}

return 0; }

#include <assert.h>

struct {
  int a:4;
  int :4;
  int b:4;
  int c:4;
} x = { 2,3,4 };

int main ()
{
  if (x.b != 3)
    {assert(0); }
return 0; }

#include <assert.h>
struct foo
{
  unsigned long long b:40;
} x;

void test1(unsigned long long res)
{
  if (x.b<<32 != res)
    {assert(0); } 
}

int main()
{
  x.b = 0x0100;
  test1(0);
  return 0;
}

CBMC version: 5.10
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc <file.c>
What behaviour did you expect:Result in SUCCESS (proofed by compiling with gcc and executing)
What happened instead:[foo.assertion.1] assertion 0: FAILURE

[kroening]

Many thanks -- I've made PRs for the first two problems.

I'll need to look a bit more into the third. gcc on Ubuntu 18.04 passes this, but clang gives a failure. This may well be implementation-defined or undefined behavior.

[muchang]

Thank you so much for your update, the third one may be the implementation-defined feature.
Here is another case related to bit-field:

#include <assert.h>
typedef struct _st {
    long int iIndex : 24;
} st;
st *next;

void f(void)
{
    int nIndx;
    const static long int constreg[] = { 0xFEFEFEFE,};
    next->iIndex = constreg[0];
}

int main(void)
{
  st a;
  next = &a;
  f();
  if (next->iIndex != 0xFFFEFEFE)
    {assert(0);} 
  return 0;
}

CBMC version: 5.10
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc <file.c>
What behaviour did you expect:Result in SUCCESS (proofed by compiling with gcc and executing)
What happened instead:[foo.assertion.1] assertion 0: FAILURE

[kroening]

I looked at the third one. I think this is undefined behavior. The bit-field should get promoted to signed long long. Then you are doing an overflowing signed left shift.

[kroening]

I.e., clang failing this is ok.

[kroening]

The problem in the "other case" has already been fixed with ab6e2d1.

[muchang]

Thank you for your confirmation! I also think the third one is undefined behavior. This issue can be closed.