locked
Static Analysis of Containers? RRS feed

  • Question

  • Consider this:

      public static class Program
      {
        private static void Main(string[] args)
        {
          var enumerable = new List<object>
          {
            " ",
            '0',
            0u,
            0ul,
            0.0f,
            0.0d,
            0.0m
          };
    
          Contract.Assume(Contract.ForAll(enumerable, x => x != null));
          PrintEnumerable(enumerable);
          Console.ReadKey();
        }
    
        private static void PrintEnumerable<T>(IEnumerable<T> list)
        {
          Contract.Requires(list != null);
          Contract.Requires(Contract.ForAll(list, x => x != null));
    
          foreach (var o in list)
            Print(o);
        }
    
        private static void Print(object o)
        {
          Contract.Requires(o != null);
    
          Console.WriteLine(o);
        }
      }
    

    Apparently, even with the Contract.Assume, the static checker refuses to believe that 'enumerable' has no null elements:

    warning : CodeContracts: requires unproven: Contract.ForAll(list, x => x != null)

    The Contract.ForAll within PrintEnumerable does, however, work correctly, as removing it yields a warning that 'o' (in the foreach) might be null.

    Is there something I'm doing incorrectly here, or is this a bug in the static checker?

    Thanks in advance.

    Wednesday, October 20, 2010 11:22 PM

Answers

  • Hi Alex,

      you are not doing anything wrong. The container analysis understands arrays, but we are still working for the other collections (as e.g. the List above).

     

    thanks,

    f

    Tuesday, February 8, 2011 9:57 PM