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

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

Pascal, I agree, it is undefined.

Xuejun, what is the status of your bug fixes for side effecting assignments?


On 07/17/2011 11:02 AM, Pascal Cuoq wrote:

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.