Re: [csmith-dev] Another union issue

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

Ok, this is fixed in commit c5b2c6 with a platform specific file that is
read/written by Csmith before the random generation. The operations are
behind the scene, and unless you are doing cross-generation, i.e.,
generation test cases on one platform then test them on another, you
shouldn't worry about the file.

thanks,
-Xuejun

> -----Original Message-----
> From: Xuejun Yang [mailto:jxyang@cs.utah.edu]
> Sent: Wednesday, August 10, 2011 4:46 PM
> To: 'John Regehr'; 'csmith-dev@flux.utah.edu'
> Subject: RE: [csmith-dev] Another union issue
> 
> 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
> > >