requires unproven: arrayIndex + this.Count <= array.Length

Question

Hello,

This warning persists even though I'm checking for it, why ?

        public void CopyTo(T[] array, int arrayIndex)
        {
            Contract.Requires(array != null);
            Contract.Requires(arrayIndex >= 0);
            Contract.Requires(arrayIndex + Count <= array.Length);
        }

---

Eyal (http://shilony.net), Regards.

Answer 1

Need a bit more information - which line is the warning coming from? If I had to guess, I'd say that the problem is with the caller of this method. Does it ensure that the parameters it passes are correct?

Answer 2

Here is the complete code, nothing is calling it yet.

namespace EasyFront.Framework.Collections.Generic
{
	using System.Collections.Generic;
	using System.Diagnostics.Contracts;

	[ContractClass(typeof(IReadOnlyCollectionContract<>))]
	public interface IReadOnlyCollection<T> : IEnumerable<T>
	{
		int Count { get; }

		bool Contains(T item);

		void CopyTo(T[] array, int arrayIndex);
	}
}

namespace EasyFront.Framework.Collections.Generic
{
	using System.Collections;
	using System.Collections.Generic;
	using System.Diagnostics.Contracts;

	[ContractClassFor(typeof(IReadOnlyCollection<>))]
	internal abstract class IReadOnlyCollectionContract<T> : IReadOnlyCollection<T>
	{
		public int Count
		{
			get
			{
				Contract.Ensures(Contract.Result<int>() >= 0);

				return default(int);
			}
		}

		IEnumerator IEnumerable.GetEnumerator()
		{
			return GetEnumerator();
		}

		public bool Contains(T item)
		{
			return default(bool);
		}

		public void CopyTo(T[] array, int arrayIndex)
		{
			Contract.Requires(array != null);
			Contract.Requires(arrayIndex >= 0);
			Contract.Requires(arrayIndex + Count <= array.Length);
		}

		public IEnumerator<T> GetEnumerator()
		{
			return default(IEnumerator<T>);
		}
	}
}

namespace EasyFront.Framework.Collections.Generic
{
	using System.Collections;
	using System.Collections.Generic;
	using System.Diagnostics.Contracts;

	public class ReadOnlyCollection<T> : IReadOnlyCollection<T>
	{
		public ReadOnlyCollection(ICollection<T> collection)
		{
			Contract.Requires(collection != null);

			Items = collection;
		}

		public int Count
		{
			get
			{
				return Items.Count;
			}
		}

		protected ICollection<T> Items { get; set; }

		IEnumerator IEnumerable.GetEnumerator()
		{
			return GetEnumerator();
		}

		public bool Contains(T item)
		{
			return Items.Contains(item);
		}

		public void CopyTo(T[] array, int arrayIndex)
		{
			Items.CopyTo(array, arrayIndex);
		}

		public IEnumerator<T> GetEnumerator()
		{
			return Items.GetEnumerator();
		}

		[ContractInvariantMethod]
		[System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Performance", "CA1822:MarkMembersAsStatic", Justification = "Required for code contracts.")]
		private void ObjectInvariant()
		{
			Contract.Invariant(Items != null);
		}
	}
}

Here is the error.

d:\My Projects\Projects\EasyFront\EasyFront.Framework\EasyFront.Framework\Collections\Generic\ReadOnlyCollection`1.cs(44,4): warning : CodeContracts: requires unproven: arrayIndex + this.Count  <= array.Length

---

Eyal (http://shilony.net), Regards.

Answer 3

Hello Eyal,

Warning is relater to the requires of "this.Items" property inherited from ICollection<T> interface not requires of IReadOnlyCollection<T>. The problem occures durring this.Items.CopyTo method call. Warrnign can be confusing, but it states that "arrayIndex + this.Count <= array.Length" cannot be proven in context of this.Items property, so "this" shall be interpreted as "this.Items". Static checker dont know "this.Count == this.Items.Count" relation.

If you add

Contract.Invariant(this.Count == this.Items.Count);

to the ObjectInvariant method the warning will be replaced with a new one:

CodeContracts: invariant unproven: this.Count == this.Items.Count

in method ReadOnlyCollection<T>.CopyTo - dont know why ICollection<T>.CopyTo is not marked as [Pure], probably there are some scenarios im not aware of.

Two "solutions" Ive found for your original warning are:

1. mark IReadOnlyCollection<T>.CopyTo as [Pure] (dont know what kind of information it gives to the static checker but the warning disappeared).

2. add Contract.Assert(ITem.Count == this.Count); at the begining of the ReadOnlyCollection<T>.CopyTo method as Contract.Assume will generate message: Assumption can be proven.

Best Regards,

  Baal

Answer 4

Thank you! ;)

EDIT: This won't do, I need to handle it in my contract class.

---

Eyal (http://shilony.net), Regards.

Answer 5

Hello,

Unfortunately you cannot handle this warning in contract class. The warning is related to Items property of ReadOnlyCollection<T> implementation which is not defined in IReadOnlyCollection<T> interface. You can check this by changing for a moment contract for IReadOnlyCollection<T>.CopyTo to something like this:

public void CopyTo(T[] array, int arrayIndex)
{
    Contract.Requires(array != null);
    Contract.Requires(arrayIndex >= 0);
    Contract.Requires(array.Length - Count => arrayIndex);
}

I've changed order and sides in last inequality. If warning is related to IReadOnlyCollection<T> interface the message will be changed to:

"CodeContracts: requires unproven: array.Length - Count => arrayIndex".

But it stays the same:

"CodeContracts: requires unproven: arrayIndex + Count <= array.Length".

It means that your IReadOnlyCollection<T> and its contract is fine, but code calling "Items.CopyTo" possibly violates contract for ICollection<T>.CopyTo method (does not ensures that "arrayIndex + Items.Count <= array.Length").

The only solution I can really think of is to add  Contract.Assert(Item.Count == this.Count); just before Items.CopyTo(array, arrayIndex); call.

Best regards,

  Baal

Answer 6

@Baal, for now I chose to ignore this error by enabling the baseline option but thank you so much for your time, help and efforts.

---

Eyal (http://shilony.net), Regards.