Code contracts static checking does not seem to be working

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


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.


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.

    链接地址: http://www.djcxy.com/p/23744.html

    上一篇: 为不执行代码合同的代码验证后置条件

    下一篇: 代码合同静态检查似乎没有工作