The following code satisfies its assertions if the compiler and processor respect strictly the IEEE-754 norm which requires that each single operation is rounded to 64bits.
Otherwise, the value of variable res might be -1.0 instead of 0.0, such as when using 80bits arithmetic for auxiliary calculations, available in x387 unit, or using FMA atomic operation. Also, if we perform deductive verification of that code with the perfect mathematical real numbers instead of floating-numbers, we also get res=-1.0.
#pragma JessieFloatModel(strict)
int main() {
double tmp= 0x1p53;
double x = tmp * (tmp - 2.0);
//@ assert x == \exact(x);
double y = tmp - 1.0;
//@ assert y == \exact(y);
double res = x - y * y;
//@ assert res == 0.0; // OK if IEEE-754, but if real mode or FMA: -1.0
printf("%g\n",res);
return 0;
}
This is proved entirely by Gappa