CodeContracts - false positives

Question

I've just started experimenting with CodeContracts in .NET 4 on an existing medium-sized project, and I'm surprised that the static checker is giving me compile-time warnings about the following piece of code:

public class Foo
{
   private readonly List<string> strs = new List<string>();

   public void DoSomething()
   {
       // Compiler warning from the static checker:
       // "requires unproven: source != null"
       strs.Add("hello");
   }
}

Why is the CodeContracts static checker complaining about the strs.Add(...) line? There's no possible way for strs to be null, right? Am I doing something wrong?

Answer 1

The field may be marked readonly, but unfortunately the static checker isn't smart enough for this. Therefore, as the static checker isn't able to infer on its own that strs is never null, you must explicitly tell it through an invariant:

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