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