错误的代码合同警告

本文关键字：警告 合同 代码 错误 | 更新日期: 2023-09-27 18:29:02

我最近为一个非常大的项目添加了代码契约。在我处理了几百个警告并添加了断言来安抚检查器之后，我留下了一些明显不正确的警告！这可能是我能做的最简单的例子（如果你认为细节可能很重要，完整的代码在这里）：

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

这个建议显然是错误的（我有单元测试从这个函数返回非null值来证明这一点）！如果"DoSomething"也总是返回null，但它并没有对此提出任何建议，那么这可能是真的。

编辑：我已经通过完全重写DoSomething方法来解决上述问题，使其不使用out结果（相反，它返回包含outResult和result的元组）。然而，我仍然有其他错误的警告，我想解决这些问题，可能有同样的根本原因。

所以实际上这是两个问题：

  1. 我是做错了什么还是遗漏了一些明显的东西
  2. 假设CC只是错误，我能做些什么来缓解未来的这种问题吗？至少要隐藏警告

错误的代码合同警告

Re:合同。确保返回值

在您的MVCE和生产代码中，在上游的"举证责任"之后，问题几乎肯定会出现在所称的SelectScript扩展方法（或MVCE中的DoSomething）上，其中静态分析器推断（可能不正确）扩展方法总是返回null，因此在调用方法SelectSingle中总是选择第一个分支（也返回null），因此推荐null的后置条件。

我找不到您的SelectScript代码，但在VS 2013更新4/CC 1.7.11202.10上，我只能通过从SelectScript显式仅返回null并启用"推断确保"静态检查选项，或者通过向SelectScript显式添加Contract.Ensures(Contract.Result<ScriptReference>() == null);来重复Contracts警告，例如通过确保推断：

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.ValueAtReturn-将契约添加到out参数中参考，第2.2.3 p8节。

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

 Contract.Ensures(Contract.ValueAtReturn(out selectedTags) == null ||
                  Contract.ValueAtReturn(out selectedTags) != null);
相关文章：