Code contracts static checking does not seem to be working

Question

I am using VS 2010 and testing something real basic :

class Program
{
    static void Main(string[] args)
    {
        var numbers = new int[2];
        numbers[3] = 0;
    }
}

I have gone to properties > Code Contracts and have enabled the static checking. No errors / warnings/squiggly underlines are showing on compile / build.

EDIT:

When turning the warning level to max I get this warning, which is not the warning I am after :

Warning 1 CodeContracts: Invoking method 'Main' will always lead to an error. If this is wanted, consider adding Contract.Requires(false) to document it

Answer 1

It's not clear what warning you're expecting (you state "I get this warning, which is not the warning I am after" without actually saying what warning you are after), but perhaps this will help.

First up:

var numbers = new int[2];
numbers[3] = 0;

This is an out-of-bounds access that will fail at runtime. This is the cause of the error you're getting, which states that "Invoking method 'Main' will always lead to an error." - that's perfectly accurate, it will always lead to an error because that out-of-bounds array access will always throw a runtime exception.

Since you state that this isn't the warning you're expecting, though, I've had to employ a bit of guesswork as to what you were expecting. My best guess was that due to having ticked the 'Implicit Non-Null Obligations' checkbox, and also having tried adding Contract.Requires(args != null) to your code, you're expecting to get a warning that your Main method could potentially be called with a null argument.

The thing is, Code Contracts will only inspect your own code to make sure that you always provide a non-null argument when calling Main. The thing is, you never call Main at all - the operating system will call Main, and Code Contracts is not going to inspect the operating system's code!

There's no way to provide compile-time checking of the arguments provided to Main - you have to check these at runtime, manually. Again, Code Contracts works by checking that calls you make to a function meet the requirements you set - if you're not actually making the calls yourself, Code Contracts has no compile-time say in the matter.

Answer 2

I have tried this (albeit with Visual Studio 2013 + Code Contracts) and I found the following:

• With the Warning Level set to "low" (like you have), I do not get a warning.
• With the Warning Level set to "hi", I do get a warning.

So I suggest increasing your warning level slider.