False positive: precondition is redundant

Question

Why do I get the following warning for this trivial code sample as soon as the Warning Level is on the 2nd level or higher?

public int Foo(int a)
{
    if (a >= 0) throw new ArgumentException("a should be negative", "a");
    Contract.EndContractBlock();
    return a;
}

CodeContracts: Suggested requires: This precondition is redundant: Consider removing it. Are you comparing a struct value to null?

Clearly an integer can be negative so the precondition is hardly redundant, so why do I get this warning?

Edit: Here is what ILSpy shows for the created function when looking at the exe:

public int Foo(int a)
{
    if (a >= 0)
    {
        ContractHelper.RaiseContractFailedEvent(ContractFailureKind.Precondition, null, "a < 0", null);
        throw new ArgumentException("a should be negative", "a");
    }
    return a;
}

Answer 1

I know this doesn't directly answer your question, but it appears you're using a legacy mode for Code Contracts.

This document describes the recommended assembly mode based on usage requirements:

http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf

From Pages 20, 21...

Another snippet from the document:

5.1.1 Assembly Mode

The contract tools need to know which usage mode you choose. If you use VisualStudio, select the Assemby Mode on the contract property pane as follows:

• Usage 1 or 2: Standard Contract Requires
• Usage 3: Custom Parameter Validation

This permits the tools to emit proper warnings when you violate the usage guidelines. If you use the tools from the command-line, pass the proper argument for the -assemblyMode option

So using "Standard Contract Requires" assembly mode you could do either of the following:

Contract.Requires<ArgumentException>(a < 0, "a");
// OR
Contract.Requires(a < 0, "a should be negative");

Neither of these generate any warnings for me.

I hope this helps anyway.

Cheers peteski