CodeContracts reports exact mismatch between two doubles

Question

Given the following C # code,

double x = 2.0;
x *= 0.5;
bool y = (x == 1.0);
Console.WriteLine(y);

CodeContracts gives a warning: Possible precision mismatch for the arguments of ==.

If I changed the code to one of the following:

double x = 2.0 * 0.5;
bool y = (x == 1.0);
Console.WriteLine(y);

or

double x = 2.0 * 0.5;
bool y;
if (x == 1.0) {
  y = true;
} else {
  y = false;
}
Console.WriteLine(y);

or perhaps most vaguely

double x = 2.0;
x *= 0.5;
bool y = ((double)x == 1.0);
Console.WriteLine(y);

he does not give me any warnings. What distinguishes the first case from others, that it deserves a warning?

Update

Another example of creating this warning, this time as a defender for the division operator:

Contract.Requires<ArgumentOutOfRangeException>(rhs != 0.0);

Answer 1

Statement

double x = 2.0 * 0.5;

Probably never executed even at run time; the compiler will simply simplify

double x = 1.0;

In addition, the equality check still does not guarantee whether the value is “exactly one”. Consider this:

double x = 100000000000.0;
x*= 0.00000000001;
Console.WriteLine(x); // Prints "1"
bool y = ((double)x == 1.0);
Console.WriteLine(y); // Prints "False"