我在和CodeContracts static analysis tool吵架。

我的代码:

c# - CodeContracts : Possibly calling a method on a null reference-LMLPHP

(ASCII version)

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

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

最佳答案

更新:似乎问题在于invariants are not supported for static fields

第二次更新:下面概述的方法是currently the recommended solution

一个可能的解决方法是为instance创建一个属性,该属性Ensure是要保留的不变量。 (当然,需要对它们进行Assume才能被证明。)完成此操作后,就可以使用该属性,并且所有不变量都应被正确证明。

这是使用此方法的示例:

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

关于c# - CodeContracts : Possibly calling a method on a null reference,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/2679395/

10-13 03:16