开发者

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

开发者 https://www.devze.com 2023-04-02 04:56 出处:网络
I have some factory method public T Create<T> () where T : class { Contract.Ensures(Contract.Result<T>() != null);

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: Contra开发者_如何学JAVAct.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.


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.


Like if((result ?? 0) == 0){}

To make this more clear (readable) you can define an extension method.

Edit

@allentracks answer is more precise for your question

0

精彩评论

暂无评论...
验证码 换一张
取 消