Diagnosing 'CodeContracts requires unproven: constructor != null'?

Question

I have several methods that report the warning "Code Contracts: requires unproven: constructor != null" when the C# CodeContracts static checker is enabled.

These particular methods do not declare any contracts, and are not called by any methods that do.

If I double-click the warnings, visual studio directs me to the line instantiating an IQueryable<TEntity> object. Here's one of the offending methods:

public List<IStudentTermData> GetAllActive()
{
    using (IObjectContext context = ContextFactory.Create())
    {
        var studentTermDataSet = context.ObjectSet<IStudentTermData>();
        var studentSet = context.ObjectSet<IStudent>();

        // Helps out CodeContracts static checker
        if(studentSet == null || studentTermDataSet == null)
            return new List<IStudentTermData>();

        // Selecting the warning brings me to the next line
        IQueryable<IStudentTermData> query =
            from studentTermData in studentTermDataSet
            join student in studentSet 
            on studentTermData.StudentId equals student.Id
            where (student.Active) select studentTermData;

        return query.ToList();
    }
}

I have several other very similar methods that do not exhibit this warning, and I noticed they do not use a LINQ join. I'm guessing that my LINQ query is being deconstructed into some (possibly null) IQueryable object that gets Join() called on it, causing this warning.

What does this have to do with the CodeContracts static checker? Also, why is the checker complaining, and what can I do to fix it?

Answer 1

There seems to be a bug here.

Your query desugars to:

IQueryable<IStudentTermData> query =
    studentTermDataSet.Join(studentSet,
                            studentTermData => studentTermData.StudentId,
                            student => student.Id,
                            (studentTermData, student) => new {studentTermData, student})
                      .Where(s => (s.student.Active))
                      .Select(std => std.studentTermData);

The only parameter called "constructor" is the last parameter of the Join method, and indeed, if you change the code to:

var query =
    studentTermDataSet.Join(studentSet,
                            studentTermData => studentTermData.StudentId,
                            student => student.Id,
                            Tuple.Create);

then it compiles without warnings.

The difference is that the first query uses the Join overload which takes an Expression as a parameter, whereas the second one takes a Func (and returns an IEnumerable).

So I think that the support for expression trees is possibly not complete yet. You could post a question on the Code Contracts forum to ask about this.