CodeContracts - 误报

Question

我刚开始在一个现有的中型项目上尝试使用.NET 4中的CodeContracts,我很惊讶静态检查器给出了关于以下代码段的编译时警告:

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");
   }
}

为什么CodeContracts静态检查器抱怨strs.Add(...)行？strs没有可能成为null的方法,对吗？难道我做错了什么？

Answer 1

可以标记该字段readonly,但遗憾的是静态检查器对此不够智能.因此,由于静态检查器无法自行推断strs永远不为null,因此必须通过不变量明确告知它:

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