Contract.ForAll doesn't work?

Question

I'm trying to use Contract.ForAll, and it looks like I'm missing something here.

Consider this small example:

        var l = new List<string>();
        Contract.Assume( Contract.ForAll( l, s => s != null ) );

        foreach ( var s in l ) Console.WriteLine( s.Length );

Despite the Contract.Assume call, I do get a "possible calling a method on a null reference" warning for s.Length.

Am I doing this right? Is it even supposed to work? Or am I missing something?

Answer 1

From the Code Contracts User Manual, section 6.6.1 Current Limitations of the Checker and Bugs:

The static contract checker does not yet deal with quantifiers ForAll or Exists.

Answer 2

Did you enable the "container analyses" option on the static checker Pane?