Re: [csmith-dev] Another union issue

["Xuejun Yang" <jxyang@cs.utah.edu>]

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?

-Xuejun

> -----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.
>   Xuejun?
> 
> John
> 
> 
> 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
assumption.
> >
> > 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}}};
> >
> > main(){
> > ...
> >      for (i = 0; i < 1; i++)
> >      {
> >          for (j = 0; j < 1; j++)
> >          {
> >              transparent_crc(g_142[i][j].f3, "g_142[i][j].f3",
> > print_hash_value);
> >              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
> > initialized.
> >
> > 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.
> >
> > Pascal
> >