LINQ query: requires unproven: constructor != null

Question

Hello,

I have a strange issue with LINQ.

class Test
    {
        public int Int1 { get; set; }
        public int Int2 { get; set; }
    }

    struct IntStruct
    {
        public IntStruct(int i1, int i2) {}
    }

    class Program
    {
        static IQueryable<Test> GetQuery()
        {
            Contract.Ensures(Contract.Result<IQueryable<Test>>() != null);
            throw new NotImplementedException();
        }

        static void Main(string[] args)
        {
            IQueryable<Test> query = GetQuery();

            var items = from q in query
                        select new
                        {
                            Struct = new IntStruct(q.Int1, q.Int2)
                        };

            Tester tester = new Tester();
            tester.RunQuery(query);
        }
    }

    class Tester
    {
        public void RunQuery(IQueryable<Test> query)
        {
            Contract.Requires(query != null);

            var items = from q in query
                        select new
                        {
                            Struct = new IntStruct(q.Int1, q.Int2)
                        };
        }
    }

The query inside Program.Main does not generate any warnings.

The query inside Tester.RunQuery raises "requires unproven: constructor != null".

Any ideas why this is happening?

Thanks,

Stephen

Answer 1

Hi Stephen,

I'm getting the warning in both methods.

It appears to be a bug in the static checker.  It's warning about C# compiler-generated code that occurs when constructing anonymous types in LINQ operators for IQueryable<T>.  Here's a small repro:

using System.Diagnostics.Contracts;
using System.Linq;

namespace ContractLabs
{
	class IQueryableLab
	{
		public void Test(IQueryable<int> query)
		{
			Contract.Requires(query != null);

			var select = query.Select(x => new { x });		// requires unproven: constructor != null
			var select2 = query.Select(_ => new object());	// No warning
		}
	}
}

Unfortunately, I don't think there's any way to suppress this warning using contracts.  You'll either have to specify ContractVerificationAttribute(false) to disable checking on the entire method, or use SuppressMessageAttribute to suppress each individual warning.

For example:

using System.Diagnostics.Contracts;
using System.Linq;

namespace ContractLabs
{
	class IQueryableLab
	{
		[System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Contracts", "Requires-13-97")]
		public void Test(IQueryable<int> query)
		{
			Contract.Requires(query != null);

			var select = query.Select(x => new { x });		// No warning
			var select2 = query.Select(_ => new object());	// No warning
		}
	}
}

You can get the exact attribute that you need from the output window after the static checker completes by adding the following switch to the Extra Static Checker Options field on the Code Contracts tab: -outputwarnmasks

- Dave

---

http://davesexton.com/blog