不正确的代码合同警告

Question

我最近在一个非常大的项目中添加了代码合同。在通过数百个警告添加断言以安抚检查器之后，我留下了一些似乎显然不正确的警告！这可能是我能做的最简单的例子（完整代码是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 方法以不使用输出结果（而是返回包含 outResult 和结果的元组）来解决上述问题。但是，我仍然有其他错误的警告需要解决，并且可能具有相同的根本原因。

其实这是两个问题：

1. 我是不是做错了什么或遗漏了一些明显的东西？
2. 假设 CC 完全是错误，我以后有什么办法可以缓解此类问题 - 至少隐藏警告！

Answer 1

Re : Contract.Ensures 关于返回值

在您的 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，例如with 确保推断：

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 和非 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 : Contract.Ensures on the out value

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

例如如果您仍然收到关于 out 参数的警告，您可以使用 grek40 的想法通过将其添加到 SelectScript 来抑制调用者中的警告：

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