Interface contract confuses static checker

Question

Assume the following simple code:

public class Foo // : IFoo
{
    private string _field;

    public string Property
    {
        get { return _field; }
    }

    private void SetField()
    {
        _field = " foo ";
    }

    private string Method()
    {
        SetField();
        return Property.Trim();
    }
}

The static checker is able to prove that Property will be not null when Method uses it.

Now, I introduce an interface along with a contract and the static checker starts complaining: "Possibly calling a method on a null reference 'this.Property'.

Is this a bug or am I missing something?

---

The code with the interface looks like this:

public class Foo : IFoo
{
    private string _field;

    public string Property
    {
        get { return _field; }
    }

    private void SetField()
    {
        _field = " foo ";
    }

    private string Method()
    {
        SetField();
        return Property.Trim();
    }
}

[ContractClass(typeof(IFooContract))]
public interface IFoo
{
    string Property { get; }
}

[ContractClassFor(typeof(IFoo))]
public abstract class IFooContract : IFoo
{
    public string Property
    {
        get { throw new System.NotImplementedException(); }
    }
}

My settings are like this:

I get the following output:

[...]
C:\{path}\CC2.cs(11,19): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.String>() == this._field);
C:\{path}\CC2.cs(16,13): message : CodeContracts: Suggested ensures: Contract.Ensures(this._field != null);
C:\{path}\CC2.cs(21,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.String>() != null);
C:\{path}\CC2.cs(21,13): message : CodeContracts: Suggested ensures: Contract.Ensures(this._field != null);
C:\{path}\CC2.cs(21,13): message : CodeContracts: Suggested ensures: Contract.Ensures(this.Property.Trim() != null);
C:\{path}\CC2.cs(21,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.String>() == this.Property.Trim());
[...]
C:\{path}\CC3.cs(33,13): warning : CodeContracts: Possibly calling a method on a null reference 'this.Property'
[...]

I am using Visual Studio 2010 Ultimate with .NET 4 as target framework.

Answer 1

Not quite an answer, but some thoughts on the question. This is not that interface contract, which confuse Code Contracts. I've managed to reproduce this with simple example without ContractClass for interface. Just change second example to simple

//Foo's declaration

public interface IFoo
{
    string Property { get; }
}

And you will get the same error. Even adding Contract.Assume(_field != null); on Property field doesn't fix it (it will fix it adding this Assume to SetField method). I didn't manage to suppress null reference exception warning with Invariants either. The only thing that worked is quite an ugly solution, where you have to provide postcondition for interface contract and give Code Contract's a hint with assume in Property field. Full code is shown below

public class Foo  : IFoo
{
    private string _field;

    public string Property
    {
        get
        {
            Contract.Assume(_field != null);
            return _field;
        }
    }

    private void SetField()
    {
        _field = " foo ";

    }

    private string Method()
    {
        SetField();
        return Property.Trim();
    }
}

---

[ContractClass(typeof(IFooContract))]
public interface IFoo
{
    string Property { get; }
}

[ContractClassFor(typeof(IFoo))]
public abstract class IFooContract : IFoo
{
    public string Property
    {
        get
        {
            Contract.Ensures(Contract.Result<string>() != null);
            throw new NotImplementedException();
        }
    }
}

Edit: As _field can be null, I suggest to use this method body to give hints to the analyser, so that it won't bother with null reference warning.

private string Method()
{
    SetField();
    Contract.Assume(Property != null);
    return Property.Trim();
}

p.s. as John Sonmez says at pluralsight training regarding Code contracts "Static analysis is a complex, mysterious task, which hardly can be worked out without hints to the analyser suing Assume method calls".