CodeContracts: Possible null reference method call

Question

I have an argument with the CodeContracts static analysis tool .

My code is:

( ASCII version )

The tool tells me that instance.bar may be an empty reference. I believe the opposite.

Who is right? How can I prove it wrong?

Answer 1

Update . The problem seems to be that invariants are not supported for static fields .

Second update: The method described below is the currently recommended solution .

A possible workaround is to create an instance property for the Ensure invariants that you want to keep. (Of course, you need to Assume them to verify Ensure .) Once you do this, you can simply use the property, and all invariants must be checked correctly.

Here is 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; } } 

Answer 2

CodeContracts is right. There is nothing to prevent you from setting instance.bar = null before calling BarLength() .

Answer 3

Your code includes a closed static initialized instance:

 private static Foo instance = new Foo(); 

Do you assume that this means that the instance constructor will always work before accessing any static method, so providing bar initialization?

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

Sequence of events:

• Call Foo.BarLength()
• Static Foo class initialization (if not completed yet)
• Static initialization of private static member instance with instance Foo
• Entrance to Foo.BarLength()

However, static class initialization is triggered only once in the application domain - and there is no lock to ensure its completion before any other static methods are called.

So you might have a scenario like this:

• Stream Alphabet: Call Foo.BarLength()
• Thread Alpha: Static Initialization of a Foo Class (if Not Completed) Launches
• Context switch
• Beta theme: calling Foo.BarLength()
• Topic beta: There is no static initialization call to the Foo class, as it is already running
• Beta theme: login to Foo.BarLength()
• Topic beta: accessing the null static member instance

The Contract Analyzer does not know that you never run the code in a multithreaded way, therefore it should be mistaken on the part of caution.

Answer 4

If you mark the bar field as read-only, it should satisfy the static analyzer that the field will never be set to anything else after ctor is executed.

Answer 5

I agree with you. instance and bar are private, so CodeContracts must know instance.bar never set to null.