Contract.Requires not preventing a null reference warning (purple squiggly)

Question

I am specifying in the constructor that the params are not null. The fields are private and there is no other code existing for static checking to wonder whether or not these fields are getting set to null.

Nevertheless, I am getting a warning from Visual Studio 2013 that they might be null.

CodeContracts: Possibly accessing a field on a null reference 'this.origin'

How can they ever be null? Is the static checker not able to figure this out, perhaps? Or am I not doing it right?

using System.Diagnostics.Contracts;

public class Link
{

    private Shape origin;
    private Shape destination;

    public Link(Shape origin, Shape destination)
    {
        Contract.Requires(origin != null);
        Contract.Requires(destination != null);
        this.origin = origin;
        this.destination = destination;
    }

    public string OriginID()
    {
        return origin.ID; // getting purple squiggly here
    }

    public string DestinationID()
    {
        return destination.ID; // getting purple squiggly here
    }

}

EDIT:

They are gone now. My question stands though, because I don't know what I did to make them go away. I did not change anything in this class nor the project settings. It's just, at the time I got the warnings, one of my tests did not pass and now, all tests pass. That's the only difference between then and now. The changes to make the test pass were in another class, not this one.

Answer 1

Dependent upon your project settings, I do not believe the static checker is always able to work out the invariants on origin and destination.

There are several approaches which could be taken to resolve this warning:

ContractInvariantMethod

Add an explicit private method attributed with the ContractInvariantMethodAttribute and makes call to Contract.Invariant, e.g:

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(origin != null);
    Contract.Invariant(destination != null);
}

This will inform the static checker that these invariants will never be violated, i.e. origin and destination will never be null.

readonly + Infer invariants for readonly

Mark both of the fields as readonly and in your code contract settings, ensure the Infer invariants for readonly option is checked for the static checker:

I personally tend to go for the ContractInvariantMethod approach but also mark my fields as readonly if they are only initialised upon instantiation, both approaches should work however.