CodeContracts: Possibly calling a method on a null reference

Question

I'm having an argument with the CodeContracts static analysis tool.

My code:

(ASCII version)

The tool tells me that instance.bar may be a null reference. I believe the opposite.

Who is right? How can I prove it wrong?

Answer 1

CodeContracts is right. There is nothing stopping you from setting instance.bar = null prior to calling the BarLength() method.

Answer 2

I agree with you. instance and bar are both private, so CodeContracts should be able to know instance.bar is never set to null.

Answer 3

If you mark the field 'bar' as readonly, that should satisfy the static analyzer that the field will never be set to anything else after the ctor executes.

Answer 4

Your code includes a private static initialized instance:

private static Foo instance = new Foo();

Are you assuming that this means the instance constructor will always have run before access to any static method, therefore ensuring bar has been initialized?

In the single threaded case, I think you're right.

The sequence of events would be:

1. Call to Foo.BarLength()
2. Static initialization of class Foo (if not already completed)
3. Static initialization of private static member instance with instance of Foo
4. Entry toFoo.BarLength()

However, static initialization of a class is only ever triggered once per App Domain - and IIRC there's no blocking to ensure it's completed before any other static methods are called.

So, you could have this scenario:

1. Thread Alpha: Call to Foo.BarLength()
2. Thread Alpha: Static initialization of class Foo (if not already completed) starts
3. Context Switch
4. Thread Beta: Call to Foo.BarLength()
5. Thread Beta: No Call to static initialization of class Foo because that's already underway
6. Thread Beta: Entry to Foo.BarLength()
7. Thread Beta: Access to null static member instance

There's no way the Contracts analyser can know that you'd never run the code in a multithreaded way, so it has to err on the side of caution.

Answer 5

Update: It seems the problem is that invariants are not supported for static fields.

2nd Update: The method outlined below is currently the recommended solution.

A possible workaround is to create a property for instance that Ensures the invariants that you want to hold. (Of course, you need to Assume them for the Ensure to be proven.) Once you have done this, you can just use the property and all the invariants should be proven correctly.

Here's your example using this method:

class Foo
{
    private static readonly Foo instance = new Foo();
    private readonly string bar;

    public static Foo Instance
    // workaround for not being able to put invariants on static fields
    {
        get
        {
            Contract.Ensures(Contract.Result<Foo>() != null);
            Contract.Ensures(Contract.Result<Foo>().bar != null);

            Contract.Assume(instance.bar != null);
            return instance;
        }
    }

    public Foo()
    {
        Contract.Ensures(bar != null);
        bar = "Hello world!";
    }

    public static int BarLength()
    {
        Contract.Assert(Instance != null);
        Contract.Assert(Instance.bar != null);
        // both of these are proven ok

        return Instance.bar.Length;
    }
}