Re: [csmith-dev] version 7d6fae9: x = x = .;

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

I believe this problem is fixed in commit cc2104. Please verify.

-Xuejun
 
> 
> This problem, and the other problem we talked about, namely "x = x++",
stem
> from the same bug. I am thinking of a solution that has least impact on
the
> way that assignments are generated in Csmith.
> 
> -Xuejun
> 
> >
> > Pascal, I agree, it is undefined.
> >
> > Xuejun, what is the status of your bug fixes for side effecting
> assignments?
> >
> > John
> >
> >
> >
> >
> >
> > On 07/17/2011 11:02 AM, Pascal Cuoq wrote:
> > > Hello,
> > >
> > > the attached program was generated after updating Csmith from Git
today.
> > > I offer that that program is defined only if the program below is
> defined:
> > >
> > > int x;
> > > int main(int argc, char **argv) {
> > >    x = x = 2;
> > >    return x;
> > > }
> > >
> > > But both Frama-C's value analysis and KCC's June version
> > > seem to think that the short version,
> > > and therefore the long version, are undefined.
> > >
> > > KCC's error message is "Unsequenced side effect on scalar
> > > object with side effect of same object". Frama-C's error message
> > > is that you should only reach the assignment with memory states
> > > in which you can prove "\separated(&  x,&  x)". That formula
> > > is equivalent to false, meaning that the value analysis thinks
> > > there is a definite problem at the assignment.
> > >
> > > I am pretty certain they are worried about the same thing,
> > > although I wouldn't like to commit myself on whether
> > > they are both right or both wrong.
> > >
> > > Pascal