Support for equality through union in the dependence graph?

[lucasccordeiro]

I'm trying to fix some bugs in the CBMC full slicer, but I got stuck in the following C program:

#include <assert.h>
#include <stdint.h>
union u
{
  uint32_t x;
   int32_t y;
   int8_t  z[4];
};
union u pass_through_union (uint32_t q)
{
  union u un;

  un.z[0] = 0x0;
  un.y = q;
  un.z[3] = 0x0;
  un.z[0] = 0x0;

  return un;
}
int main (void)
{
  uint32_t q;
  __CPROVER_assume((q & q - 1) == 0);
  __CPROVER_assume(256 <= q && q <= (1 << 23));
  union u un = pass_through_union(q);
  assert(q == un.y);
  return 1;
}

It seems that CBMC field-sensitive program dependence analysis is not fully supporting unions. Is there some data/control dependencies missing in the pass_through_union function?

I have used the following commands to check the data/control dependencies for this particular C program:

$goto-cc main.c -o main.goto
$goto-instrument main.goto --show-dependence-graph