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

Question

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

c#visual-studio-2010.net-4.0code-contracts

7

我正在与CodeContracts静态分析工具争论。

我的代码：

这段文字的翻译如下：

(ASCII 版本)

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

谁是对的？我怎样才能证明它是错的？

- dtb

2

离题了，但你能告诉我你正在使用哪个Visual Studio主题吗？ - Justin

1

@Justin：只是默认的vs2010主题，加上我自己定制的文本颜色方案（请参见编辑后的帖子）。您为什么要问？ - dtb

最近我一直在寻找改变自己的 Visual Studio 颜色方案，我非常喜欢你的方案。不知道你是否在某个地方下载了它。 - Justin

@Justin：嗯...在我编辑之前，“主题”只是默认的StackOverflow语法突出显示方案（我相信这是基于默认的Visual Studio文本颜色方案）。您可以使用此工具为Visual Studio生成漂亮的配色方案：http://www.frickinsweet.com/tools/Theme.mvc.aspx - dtb

谢谢，我现在可能看起来有点疯狂。原来昨天我安装了一个谷歌浏览器扩展程序，可以突出语法，并且忘记了它。哈哈。抱歉浪费了你的时间。还有感谢提供链接！ - Justin

5个回答

2

CodeContracts是正确的。在调用BarLength()方法之前，没有任何阻止您设置instance.bar = null。

- EMP

2

但是我没有在任何地方设置 instance.bar = null，而且 instance.bar 是私有的，所以它不可能为空，对吧？ - dtb

是的，如果那就是整个代码，我想你是正确的。它的静态分析可能不够智能，无法确定您是否将值设置为null，因此它假设您可能会这样做。我不知道它为此付出了多少努力 - 如果有的话。 - EMP

我该如何让它相信instance.bar永远不会是null？将bar设置为只读并在构造函数中添加Contract.Ensures(bar != null);并不能解决问题。在BarLength()中使用Contract.Assume(instance.bar != null);可以解决问题，但看起来很丑。 - dtb

添加一个类不变量也没有帮助。 - dtb

1

在访问之前检查是否为空会使其更可靠（当然，这样做会有一些运行时成本）。 - Noah Richards

除了 bar 是只读的这个事实之外，没有任何阻止你在调用 BarLength() 方法之前设置 instance.bar = null。 - Robert Noack

2

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

private static Foo instance = new Foo();

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

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

事件序列将如下所示：

1.调用Foo.BarLength() 2.初始化类Foo的静态部分（如果尚未完成）

3.使用Foo的实例初始化私有静态成员instance 4.进入Foo.BarLength() 然而，类的静态初始化仅在每个应用程序域中触发一次，并且我IRC没有阻塞以确保在调用任何其他静态方法之前完成。

因此，你可能会遇到以下情况：

1.线程Alpha：调用Foo.BarLength() 2.线程Alpha：类Foo的静态初始化（如果尚未完成）开始

3.上下文切换

4.线程Beta：调用Foo.BarLength() 5.线程Beta：不需要调用类Foo的静态初始化，因为那已经在进行中

6.线程Beta：进入Foo.BarLength() 7.线程Beta：访问null静态成员instance 合同分析器无法知道您永远不会以多线程方式运行代码，因此必须谨慎处理。

- Bevan

没错，正如您所说（步骤7），instance 将为 null，而不是 instance.bar。instance.bar 只有在 Foo 实例的构造函数中分配之前才为 null，但实例仅在构造函数完成后严格存储在字段中。 - dtb

无论如何，这显然是静态分析器的限制。现在我正在寻找最好的方法来说服它我是正确的。用“假设”语句或永远不会发生的检查来弥补我的代码感觉很不舒服。 - dtb

是的，CLR确保在引用该类上的任何其他内容之前完成静态构造函数，除非您有两个相互引用静态构造函数的类：http://msdn.microsoft.com/en-us/library/aa645612.aspx - EMP

谢谢提供链接 - 它显示在单线程情况下，您必须设置循环引用；然而，它对我上面记录的多线程情况没有任何说明。不幸的是，我一直找不到我的原始参考资料 - 那是我一段时间前读到的一个奇怪的边缘案例。 - Bevan

0

如果您将字段“bar”标记为只读，那么静态分析器应该会满足该字段在构造函数执行后不会被设置为其他任何值的要求。

- anelson

将bar标记为只读没有任何效果。由于某种原因，分析器似乎没有意识到我在构造函数中将bar赋值给一个非空值。 - dtb

-1

我同意你的观点。instance和bar都是私有的，所以CodeContracts应该能够知道instance.bar永远不会被设置为null。

- Matthew Flaschen

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- porges · Accepted Answer

更新：问题似乎是不支持静态字段的不变量。

第二次更新：下面概述的方法目前是推荐的解决方案。

一种可能的解决方法是为instance创建一个属性，该属性Ensure了您想要保持的不变量。（当然，您需要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;
    }
}