Static checker on Async methods

Question

Hi,

Please review the following code:

using System.Diagnostics.Contracts;
using System.Threading;
using System.Threading.Tasks;

namespace ClassLibrary1
{
    [ContractClass(typeof(MyClassContact))]
    public interface IMyClass
    {
        Task GetTask();
    }

    [ContractClassFor(typeof(IMyClass))]
    [ContractVerification(false)]
    public abstract class MyClassContact : IMyClass
    {
        Task IMyClass.GetTask()
        {
            Contract.Ensures(Contract.Result<Task>() != null);
            return null;
        }
    }

    public class MyClassRegular : IMyClass
    {
        public Task GetTask()
        {
            return Task.Run(() => Thread.Sleep(100));
        }
    }

    public class MyClassAsync : IMyClass
    {
        public async Task GetTask()
        {
            await Task.Run(() => Thread.Sleep(100));
        }
    }
}

When running the static checker on the above code, I get the following warnings:

C:\temp\ConsoleApplication5\ClassLibrary1\MyClass.cs(28,13): warning : CodeContracts: ensures unproven: Contract.Result<Task>() != null
C:\temp\ConsoleApplication5\ClassLibrary1\MyClass.cs(19,13): warning :   + location related to previous warning
(1,1): warning : CodeContracts: ClassLibrary1.MyClassAsync.GetTask()[0x39]: ensures unproven: Contract.Result<Task>() != null
C:\temp\ConsoleApplication5\ClassLibrary1\MyClass.cs(19,13): warning :   + location related to previous warning

Both implementations obviously return non-null results.

Is this an issue with the static checker or am I missing something?

I am using Code Contracts version 1.4.50910.0 on VS2012 targeting .NET 4.5.

Answer 1

yep, this is a known limitation of the static checker: we need to do some work to support contracts with async/await

f

Answer 2

Thanks for your answer.

Could you please also comment regarding the warning I get for the "regular" implementation, which simply returns a Task (without the "async" keyword)?

Why does the static checker say that the "Ensures" is unproven on that implementation?

Answer 3

yes, of course. Task.Run(...) is new in .NET 4.5 and we did not have a contract for it, so I've added it

Thanks

f

Answer 4

OK. Thanks for the reply!