我最近将代码合同添加到一个非常大的项目中。在通过数百条警告并添加断言以使检查器平静之后,我留下了一些警告,这些警告似乎显然是错误的!这可能是我可以做的最简单的示例(如果您认为详细信息很重要,则完整代码为here):

protected Thing DoStuff(A a)
{
    Contract.Requires(a != null);
    //CodeContracts: Consider adding the postcondition Contract.Ensures(Contract.Result<Thing>() == null); to provide extra-documentation to the library clients

    D outResult;
    var result = DoSomething(a, out outResult);
    if (result == null)
        return null;

    return new Thing(outResult, result);
}


这个建议显然是错误的(我有单元测试从该函数返回非空值来证明这一点)!唯一可以实现的方法是,如果“ DoSomething”也总是返回null,但是对此没有任何建议。

编辑:我通过完全重写DoSomething方法而不使用out结果来解决了上述问题(相反,它返回包含outResult和result的元组)。但是,我还有其他一些错误警告需要解决,并且可能有相同的根本原因。

因此,实际上这是两个问题:


我在这里做错了什么还是错过了明显的事情?
假设CC完全是错误的,将来我能做些什么来缓解此类问题-至少要隐藏警告!

最佳答案

Re:Contract.Ensure on return value

在您的MVCE和生产代码中,都遵循上游的“举证责任”,几乎可以肯定会遇到所谓的SelectScript扩展方法(或MVCE中的DoSomething),在该方法中,静态分析器已推断(可能不正确) ),扩展方法始终返回null,因此在调用方法SelectSingle中,将始终选择第一个分支(也返回null),因此建议将null作为后置条件。

我找不到用于SelectScript的代码,但是在VS 2013更新4 / CC 1.7.11202.10上,我只能通过显式地从SelectScript仅返回null并启用“推断确保”静态检查选项来重复合同警告。 ,或者通过将Contract.Ensures(Contract.Result<ScriptReference>() == null);显式添加到SelectScript中,例如可以确保推断:

public static ScriptReference SelectScript(
    this IEnumerable<KeyValuePair<float, KeyValuePair<string, string>[]>> tags,
    Func<double> random,
    Func<KeyValuePair<string, string>[], Type[], ScriptReference> finder,
    out KeyValuePair<string, string>[] selectedTags,
    Type t)
{
    selectedTags = null;
    return null;
}


在调用方法SelectSingle中产生相同的警告:


  CodeContracts:考虑添加后置条件Contract.Ensures(Contract.Result()== null);向图书馆客户提供额外的文件资料


但是,对我来说,分析器确实可以正确地推断出以下代码具有分支,它们都返回null和non-null,并且不建议调用者使用前提条件:

    public static ScriptReference SelectScript(
        this IEnumerable<KeyValuePair<float, KeyValuePair<string, string>[]>> tags,
        Func<double> random,
        Func<KeyValuePair<string, string>[], Type[], ScriptReference> finder,
        out KeyValuePair<string, string>[] selectedTags,
        Type t)
    {
        Contract.Requires(random != null);

        selectedTags = null;
        return (random() > 0.5)
            ? null
            : new ScriptReference();
    }


Re:合同。确保超出价值

出于兴趣,还可以使用out将合同添加到Contract.ValueAtReturn参数-
reference,第2.2.3节p8。

例如如果仍在out参数上收到警告,则可以使用grek40的想法通过将其添加到SelectScript来抑制调用方中的警告:

 Contract.Ensures(Contract.ValueAtReturn(out selectedTags) == null ||
                  Contract.ValueAtReturn(out selectedTags) != null);

关于c# - 不正确的代码契约(Contract)警告,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/34603765/

10-09 19:57
查看更多