Why I still get Code Contracts : Ensure unproven warning?

Question

Below is a very simple example. When I turn on the static analysis warnings, I still get Warning CodeContracts: ensures unproven: Contract.Result() != string.Empty

on the line

return string.Format("{0}, {1}", movie.Title, movie.Description);

Please see my below code

namespace CodeContractsSamples
{
    public class MovieRepo
    {
        public string GetMovieInfo(Movie movie)
        {
             Contract.Requires(movie != null);
             Contract.Ensures(Contract.Result<string>() != string.Empty);

             return string.Format("{0}, {1}", movie.Title, movie.Description);
         }
     }

      public class Movie
      {
         public string Title { get; set; }
         public string Description { get; set; }
      }
}

Any ideas?

Answer 1

This is a limitation of the implementation of Contracts in the mscorlib dll.

See this link on the official Code Contracts forum.

This is because the contract for string.Format doesn't ensure that its result is non-empty, only that it is non-null.

Edit Some proof to back this up: When you use Reflector on the mscorlib.Contracts.dll, you can see the contracts which are defined on String.Format

[Pure, Reads(ReadsAttribute.Reads.Nothing)]
public static string Format(string format, object[] args)
{
    string str;
    Contract.Requires((bool) (format != null), null, "format != null");
    Contract.Requires((bool) (args != null), null, "args != null");
    Contract.Ensures((bool) (Contract.Result<string>() != null), null, "Contract.Result<String>() != null");
    return str;
}

As you can see, the Contract.Result statement is only non-null, not non-empty.