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

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

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