How to make Code Contracts believe that variable is not null?

Question

I have some factory method

    public T Create<T> () where T : class 
    {
        Contract.Ensures(Contract.Result<T>() != null);

        T result = this.unityContainer.Resolve<T>();

        return result;
    }

The I try to build the project i get the warning:

CodeContracts: ensures unproven: Contract.Result() != null

I understand that IUnityContainer interface does not have any contracts so Code Contracts think that varible may be null and there is no way to prove that Create() will return not null result.

How in this case I can make Code Contracts belive that result variable is not null?

I first tried to call Contract.Assert

    public T Create<T> () where T : class 
    {
        Contract.Ensures(Contract.Result<T>() != null);

        T result = this.unityContainer.Resolve<T>();

        Contract.Assert(result != null);

        return result;
    }

But it takes me another warning:

CodeContracts: assert unproven

I tried make check for null and this makes all warnings gone:

    public T Create<T> () where T : class 
    {
        Contract.Ensures(Contract.Result<T>() != null);

        T result = this.unityContainer.Resolve<T>();

        if (result == null)
        {
            throw new InvalidOperationException();
        }

        return result;
    }

But i'm not sure this is good solution to throw exception manually. May be there is some way to solve problem using Code Contracts only?

Thank you.

Answer 1

I think you want Contract.Assume:

Contract.Assume(result != null);

From the docs:

Instructs code analysis tools to assume that the specified condition is true, even if it cannot be statically proven to always be true.

This will still validate the result at execution time if you have the rewriter appropriately configured.