Why does static analysis ignore double <= and >= requirement?

Question

I have a very simple class utilizing .NET Code Contracts:

public class ContractSquareRoot
{
    /// <summary>
    /// Makes your life much easier by calling Math.Sqrt for you. Ain't that peachy.
    /// </summary>
    /// <param name="value">The value to calculate the square root from. No negatives!</param>
    /// <returns>The square root of the given value. Obviously always > 0.</returns>
    public double CalculateSquareRoot(double value)
    {
        Contract.Requires<ArgumentException>(0 <= value);
        Contract.Ensures(0 <= Contract.Result<double>());

        double squareRoot = Math.Sqrt(value);

        return squareRoot;
    }
}

When I call the method with a negative value, I expect the static code analysis to warn me about it.

class Program
{
    static void Main(string[] args)
    {

        var barMansSquareroot = new ContractSquareRoot();

        // This should not be possible...
        barMansSquareroot.CalculateSquareRoot(-42);

    }
}

But even if the Contract.Requires fails throwing the desired exception, the static code analysis marks every assertion as correct. Interestingly enough, it warns me about the violation when I change the type of value to int or if I replace <= with <. The misbehaviour is limited to double and float. I am assuming it has something to do with the precision of floating point values.

It even works when I formulate the requirement like this:

Contract.Requires<ArgumentException>(!(0 > value));

Is that a bug or am I doing something wrong?

Answer 1

I hope you might missed to install Microsoft code contract.

You can download Microsoft Code Contracts from Microsoft Research: http://research.microsoft.com/en-us/projects/contracts/

Now on your project properties you will get an extra tab where you can set runtime and static checking.