Code contracts warns about parameter when calling overloaded method

Question

I've this code (very stripped down):

[ContractClass(typeof (QueryServiceContract))]
public interface IQueryService
{
    IEnumerable<Document> ExecuteQuery(IMultiIndexQuery multiIndexQuery);

    IEnumerable<T> ExecuteQuery<T>(IMultiIndexQuery multiIndexQuery) where T : class;
}

[ContractClassFor(typeof (IQueryService))]
public abstract class QueryServiceContract : IQueryService
{
    public IEnumerable<Document> ExecuteQuery(IMultiIndexQuery multiIndexQuery)
    {
        Contract.Requires(multiIndexQuery != null);
        Contract.Ensures(Contract.Result<IEnumerable<Document>>() != null);
        return null;
    }

    public IEnumerable<T> ExecuteQuery<T>(IMultiIndexQuery multiIndexQuery) where T : class
    {
        Contract.Requires(multiIndexQuery != null);
        Contract.Ensures(Contract.Result<IEnumerable<T>>() != null);
        return null;
    }
}

public class QueryService : IQueryService
{
    public IEnumerable<Document> ExecuteQuery(IMultiIndexQuery multiIndexQuery)
    {
        throw new NotImplementedException();
    }

    public IEnumerable<T> ExecuteQuery<T>(IMultiIndexQuery multiIndexQuery) where T : class
    {
        ExecuteQuery(multiIndexQuery); // This is the row code contracts complain about.
        throw new NotImplementedException();
    }
}

public class Document
{
}

public interface IMultiIndexQuery
{
}

Code contracts give me this warning: CodeContracts: requires unproven: multiIndexQuery != null

Why do I get that warning? The QueryServiceContract has set up a contract for that parameter not being null. Both in calling and the called method...

Answer 1

I got lost while reading this code too...
Are you sure it isn't going into unbounded recursion?

As a test I renamed 1 of the ExecuteQuery() overloads (in several places):

 IEnumerable<Document> ExecuteQuery2(IMultiIndexQuery multiIndexQuery);

And that satisfies the checker.

So maybe you found a weakness in the analyzer, but before reporting it I would make sure the code works as expected.