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