Unable to prove not null in ICollection

Question

Hi all,

In method ValuesAsCollection below, the static analyzer issues a warning 'ensures unproven: Contract.ForAll(Contract.Result<ICollection<TValue>>(), v => v != null)'. What assumption should be added to remove the warning?

In method ValuesAsArray, the analyzer does not issue a warning.

Any help is greatly appreciated.

Best regards, Ranco

using System.Collections.Generic;
using System.Diagnostics.CodeAnalysis;
using System.Diagnostics.Contracts;
using System.Linq;

namespace NotNullEnsures
{
   public class Class1<TKey, TValue> where TValue : class
   {
      public TValue[] ValuesAsArray()
      {
         Contract.Ensures(Contract.Result<TValue[]>() != null);
         Contract.Ensures(Contract.ForAll(Contract.Result<TValue[]>(), v => v != null));

         TValue[] values = _inner.Values.ToArray();

         Contract.Assume(Contract.ForAll(values, v => v != null));

         return values;
      }

      public ICollection<TValue> ValuesAsCollection()
      {
         Contract.Ensures(Contract.Result<ICollection<TValue>>() != null);
         Contract.Ensures(Contract.ForAll(Contract.Result<ICollection<TValue>>(), v => v != null));

         ICollection<TValue> values = _inner.Values;

         Contract.Assume(Contract.ForAll(values, v => v != null));

         return values;
      }

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

      private readonly Dictionary<TKey, TValue> _inner = new Dictionary<TKey, TValue>();
   }
}

Answer 1

For some reason (== bug), we cannot see the Contract.ForAll in the second case.

Until we fix the bug, the best thing is just to use the SuppressMessage attribute to mask the warning