How to avoid "source !=null" when using Code Contracts and Linq To Sql?

Question

I have the following code using a normal data context which works great:

var dc = new myDataContext();
Contract.Assume(dc.Cars!= null);
var cars = (from c in dc.Cars
            where c.Owner == 'Jim'
            select c).ToList();

However when I convert the filter to an extension method like this:

var dc = new myDataContext();
Contract.Assume(dc.Cars!= null);
var cars = dc.Cars.WithOwner('Jim');

public static IQueryable<Car> WithOwner(this IQueryable<Car> cars, string owner)
{
    Contract.Requires(cars != null);
    return cars.Where(c => c.Owner == owner);
}

I get the following warning:

warning : CodeContracts: requires unproven: source != null

Answer 1

My guess is that your warning is caused by the owner parameter, rather than the cars. Add a precondition in the WithOwner method to check if owner is not null.

public static IQueryable<Car> WithOwner(IQueryable<Car> cars, string owner)
{
    Contract.Requires(cars != null);
    Contract.Requires(!string.isNullOrEmpty(owner));
    return cars.Where(c => c.Owner = owner);
}

In your first code sample, you have 'Jim' hard-coded, so no problems there because there is not something which can be null.

In your second example you created a method for which the static compiler cannot prove that the source ( being owner ) 'will never be null', as other code might call it with an invalid values.

Answer 2

I wonder how you get the code compiled with the Extension method since you are missing this keyword in your method signature.

public static IQueryable<Car> WithOwner(this IQueryable<Car> cars, string owner)
{
    ...
}

/KP