Incorrect Code Contracts Warnings

Question

I have recently added code contracts to a very large project. After working my way through a few hundred warnings adding assertions to pacify the checker I am left with some warnings which appear to be obviously incorrect! This probably the most simple example I can make (full code is here, if you think the details may be important):

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

This suggestion is quite clearly wrong (I have unit tests which return non-null values from this function to prove it)! The only way it could be true is if "DoSomething" also always returns null, but it is not making any suggestion regarding that.

Edit: I have fixed the above problem by totally rewriting the DoSomething method to not use an out result (instead it returns tuple containing both outResult and result). However I still have other false warnings which I would like to solve and probably have the same root cause.

So really this is two questions:

1. Am I doing something wrong or missing something obvious here?
2. Assuming CC is simply wrong is there anything I can do to mitigate this kind of problem in the future - at the very least hide the warning!

Answer 1

Re : Contract.Ensures on the return value

In both your MVCE and production code, following the 'burden of proof' upstream, the issue will almost certainly be with the called SelectScript extension method (or DoSomething in the MVCE), where the static analyzer has inferred (possibly incorrectly) that the extension method always returns null, and hence that in the calling method SelectSingle that the first branch (also returning null) would always be chosen, hence the recommended postcondition for null.

I can't find your code for SelectScript, but on VS 2013 update 4 / CC 1.7.11202.10, I can only repeat the Contracts warning by explicitly returning only null from SelectScript and enabling the "Infer ensures" static checking option, OR by explicitly adding a Contract.Ensures(Contract.Result<ScriptReference>() == null); to SelectScript, e.g. with ensures inference on:

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

Produces the same warning in the calling method SelectSingle:

CodeContracts: Consider adding the postcondition Contract.Ensures(Contract.Result() == null); to provide extra-documentation to the library clients

However, for me, the analyzer does appear to correctly infer that the below code has branches which both return null, and non-null, and doesn't recommend the precondition in the caller:

    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

Out of interest, it is also possible to add contracts to out parameters, by using Contract.ValueAtReturn - reference, section 2.2.3 p8.

e.g. If you are still receiving the warning on the out parameter, you could use grek40's idea to suppress the warnings in the caller by adding this to SelectScript:

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