How do I indicate that a method never returns a null using code contracts?

Question

How do I indicate that a method never returns a null? Currently this is my code.

Line 19 gets an Ensures not proven message, even though CreateFunction assumes that the result is not nothing.

1         <Pure()> Public Function CreateFunction(Of TArg1, TArg2, TResult)(ByVal body As Func(Of Expression, Expression, BinaryExpression)) As Func(Of TArg1, TArg2, TResult)   
2             Contract.RequiresAlways(body IsNot Nothing)   
3             Contract.Assume(Contract.Result(Of Func(Of TArg1, TArg2, TResult))() IsNot Nothing)   
4   
5             Dim arg1 = Expression.Parameter(GetType(Integer), "arg1")   
6             Dim arg2 = Expression.Parameter(GetType(Integer), "arg2")   
7   
8   
9             Dim temp = Expression.Lambda(body(arg1, arg2), arg1, arg2)   
10             Contract.Assume(temp IsNot Nothing)   
11             Return DirectCast(temp.Compile, Global.System.Func(Of TArg1, TArg2, TResult))   
12         End Function  
13   
14         <Pure()> Public Function Add() As Func(Of T, T, T)   
15             Contract.Ensures(Contract.Result(Of Func(Of T, T, T))() IsNot Nothing)   
16   
17             Dim temp = CreateFunction(Of T, T, T)(AddressOf Expression.AddChecked)   
18             Return temp   
19         End Function  

Answer 1

Does

Contract.Ensures(Contract.Result() != null);

work? Basically, I'd try paring it down till you find the simplest case that doesn't work as you'd expect and go from there.

-- MarkusQ

Answer 2

You need to change the Assume in CreateFunction to an Ensures. After that you should be okay. Remember, Assume is for internal assumptions in order to help the static checker locally. They are not visible from other methods. Only Requires and Ensures are cross-method contracts.