CodeContracts：可能在空引用上调用方法答案

【问题标题】：CodeContracts: Possibly calling a method on a null referenceCodeContracts：可能在空引用上调用方法
【发布时间】：2010-04-20 23:27:02
【问题描述】：

我与CodeContracts static analysis tool 发生争执。

我的代码：

(ASCII version)

该工具告诉我instance.bar 可能是空引用。我相信相反。

谁是对的？我如何证明它是错误的？

【问题讨论】：

离题，但你能告诉我你使用的是什么视觉工作室主题吗？
@Justin：只是默认的 vs2010 主题和我自己的自定义文本配色方案（请参阅编辑后的帖子）。为什么要问？
我最近一直在寻找改变我自己的视觉工作室配色方案，真的很喜欢你的。我想知道你是否在某个地方下载了它。
@Justin：嗯...我编辑之前的“主题”只是默认的 StackOverflow 语法突出显示方案（我相信它基于默认的 Visual Studio 文本颜色方案）。您可以使用此工具为 Visual Studio 生成漂亮的配色方案：frickinsweet.com/tools/Theme.mvc.aspx
谢谢，我现在可能看起来有点疯狂。原来我昨天安装了一个 google chrome 扩展程序，它突出了语法并忘记了它。哈哈。很抱歉浪费您的时间。并感谢您的链接！

标签： c# visual-studio-2010 .net-4.0 code-contracts

【解决方案1】：

更新：看来问题出在invariants are not supported for static fields。

第二次更新：下面列出的方法是currently the recommended solution。

一种可能的解决方法是为instance 创建一个属性，Ensures 是您想要保留的不变量。（当然，您需要Assume 他们才能证明Ensure。）完成此操作后，您就可以使用该属性，并且所有不变量都应该被正确证明。

这是您使用此方法的示例：

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

【讨论】：

感谢您对此进行调查。如果您对它感兴趣，请随时将其发布到 MSDN 论坛。我现在已经停止使用静态检查器，因为代码审查目前对我来说会产生更好的结果。
我在论坛上发现了一个帖子，指出静态字段不支持不变量。我已经用解决方法更新了我的帖子。
不错的发现。但是bar 是一个实例字段，不是静态的！？无论如何，我已将复选标记移至此答案，因为这是迄今为止最好的解释。
我认为问题在于instance 是静态的，因此通过它访问的任何字段也不起作用。我实际上已经收到了其中一个团队的回复，看来我想出的解决方案是（当前）推荐的静态字段解决方案。

【解决方案2】：

CodeContracts 是对的。在调用BarLength() 方法之前，没有什么可以阻止您设置instance.bar = null。

【讨论】：

但是我没有在任何地方设置instance.bar = null，而且instance.bar 是私有的，所以它不能为空，对吧？
是的，所以如果这是整个代码，我想你是对的。它的静态分析可能不够聪明，无法确定您是否曾将该值设置为 null，因此它假设您可能。我不知道要检查多长时间 - 如果有的话。
我如何说服instance.bar 永远不是null？将bar 设为只读并将Contract.Ensures(bar != null); 添加到构造函数并不能解决问题。 Contract.Assume(instance.bar != null); in BarLength() 可以工作，但看起来很难看。
添加类不变量也无济于事。
在访问它之前检查 null 会让人信服（当然，这样做的运行时成本很小）。

【解决方案3】：

您的代码包含一个私有静态初始化实例：

private static Foo instance = new Foo();

您是否假设这意味着 instance 构造函数将始终在访问任何静态方法之前运行，从而确保 bar 已被初始化？

在单线程的情况下，我认为你是对的。

事件的顺序是：

致电Foo.BarLength()
Foo 类的静态初始化（如果尚未完成）
私有静态成员instance 的静态初始化，实例为Foo
进入Foo.BarLength()

然而，一个类的静态初始化只在每个 App Domain 中触发一次 - 并且 IIRC 在调用任何其他静态方法之前没有阻塞以确保它完成。

所以，你可以有这样的场景：

线程 Alpha：调用 Foo.BarLength()
线程 Alpha：类 Foo 的静态初始化（如果尚未完成）开始
上下文切换
线程测试版：调用Foo.BarLength()
线程 Beta：没有调用类 Foo 的静态初始化，因为这已经在进行中
线程 Beta：Foo.BarLength() 的条目
线程测试版：访问null静态成员instance

合同分析器无法知道您永远不会以多线程方式运行代码，因此必须谨慎行事。

【讨论】：

对，但正如您所说（第 7 步），instance 将为空，而不是 instance.bar。 instance.bar 只是在 Foo 实例的构造函数中赋值之前为空，但实例仅在构造函数完成后严格存储在字段中。
无论如何，这显然是静态分析器的限制。现在我正在寻找最好的方法来说服它我是对的。用Assume 语句或永远不会发生的检查乱扔我的代码感觉很脏。
是的，CLR 确实确保静态构造函数在该类上的任何其他内容被引用之前完成，除非您有两个具有相互引用的静态构造函数的类：msdn.microsoft.com/en-us/library/aa645612.aspx
感谢您的链接 - 它表明在单线程情况下您必须设置循环引用；但是，它没有说明我在上面记录的多线程案例。不幸的是，我一直找不到我的原始参考资料——这是我前段时间读到的一个奇怪的边缘案例。

【解决方案4】：

如果您将字段 'bar' 标记为只读，则应满足静态分析器的要求，即在 ctor 执行后该字段将永远不会设置为其他任何内容。

【讨论】：

将bar 标记为只读无效。出于某种原因，分析器似乎没有意识到我将 bar 分配给构造函数中的非空值。

【解决方案5】：

我同意你的看法。 instance 和 bar 都是私有的，因此 CodeContracts 应该能够知道 instance.bar 永远不会设置为 null。

【讨论】：