[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [csmith-dev] Another union issue

I'd rather you didn't add random command-line options regarding implementation-defined behavior.

Rather, please parse a file output by for example CIL's implementation-defined behavior checker.


On 08/10/2011 04:45 PM, Xuejun Yang wrote:
Yes, it is a Csmith bug. It is because this macro " _CSMITH_BITFIELD" makes
the length of bit-fields nondeterministic at generation time, and misleads
the analyzer. Is it ok I remove the macro and add a command line option
--int-bytes to solve the problem that the macro was originally designed for?


-----Original Message-----
From: csmith-dev-bounces@flux.utah.edu
[mailto:csmith-dev-bounces@flux.utah.edu] On Behalf Of John Regehr
Sent: Wednesday, August 10, 2011 4:05 PM
To: csmith-dev@flux.utah.edu
Subject: Re: [csmith-dev] Another union issue

Pascal, it looks to me like the program fragment you sent is undefined.


On 8/10/11 2:48 PM, Pascal Cuoq wrote:
Hello again,

Xuejun wrote:
  >  this is fixed in commit a39f3c. Thanks for catching my wrong

I must attest that I have been running tests based on a39f3c
since it was committed, and the issue is gone. I believe this
new question is about something else, and again, I am not
confident what is right. I have upgraded to f0ba611, the latest version.
It is again about unions and initialization.

The attached program can be reduced to the following from the
point of view of my problem:

union U3 {
     const unsigned f0 : _CSMITH_BITFIELD(41);
     const signed : _CSMITH_BITFIELD(0);
     int8_t * const  f1;
     int64_t  f2;
     const uint32_t  f3;

static union U3 g_142[1][1] = {{{1UL}}};

      for (i = 0; i<  1; i++)
          for (j = 0; j<  1; j++)
              transparent_crc(g_142[i][j].f3, "g_142[i][j].f3",
              if (print_hash_value) printf("index = [%d][%d]\n", i, j);


There is an assignment to g_142[0][0].f2 in the original, but you can
check by inserting exit(1); right before it that it is not reached.
So field f0 of g_142[0][0] is initialized, and much late, member f3 is
passed to transparent_crc().

Is that supposed to be defined?

I tried to get the information from C99's 6.7.8 section, but it is not
clear to me. However, objects are initialized according to their types:
pointers to NULL and integers to zero. An union can have both and
integer member and a pointer member. And NULL's representation does not
have to be the same as that of the integer zero. So I do not see how
6.7.8 could be saying that more than one member of an union should be

What do you think?

One argument to be made is that the program is in any case safe in
practice on desktop architectures where NULL and 0 have the same
representation, made of zeroes, and static variables are mapped to a
segment that contains only zeroes. It wouldn't be to hard to have an
option in Frama-C to implement the same point of view.