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

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

var dc = new myDataContext();
Contract.Assume(dc.Cars!= null);
var ca开发者_StackOverflowrs = (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

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.

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

Its possible that your code snippet does not completely describe the code you are using.

Consider this snippet instead:

var dc = new myDataContext();
Contract.Assume(dc.Cars!= null);
var models = dc.Cars.WithOwner('Jim').Select(c => c.Model);

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

In this snipped its likely the runtime will complain with the warning you mentioned, but it is not complaining about Cars possibly being null, it is complaining about the result from WithOwner (passed into Select) possibly being null.

You can satisfy the runtime by ensuring that the result from your extension method will not be null:

Contract.Ensures(Contract.Result<IQueryable<Car>>() != null);

This contract should be ok because Where will not return null, but instead returns an Enumerable.Empty<T>() when there are no matches.

We fixed this a few releases back. The warning was due to some missing contracts around Linq expression construction etc. Linq expression methods have contracts and the C# compiler generates code that calls these methods. If we don't have enough post conditions on the called methods, then you can get these cryptic warnings about code that you don't even know is there (unless you look with ILdasm).