Search code examples
c#code-contracts

Static Checker not proving parameters != null

When I learned about Code Contracts, I assumed I could do the following:

public void ContractTest(string input)
{
    Contract.Requires(input != null);
}

public void ContractTestCaller(string input)
{
    this.ContractTest(input);
}

And get a warning since it is not possible to prove input != null in ContractTestCaller. However I don't get a warning.
Then I thought I might at least get a warning when I do this:

public void ContractTestCallerCaller()
{
    this.ContractTestCaller(null);
}

But again, nothing.

I see three different possibilites:

  1. I'm doing something wrong.
  2. Code Contracts is not supposed to do this.
  3. The static checker is just not very good.

Which one is it?

Here are my settings:

enter image description here

Solution

  • Turns out the issue is the "Infer Requires" option being checked. I do not completely understand why but it works when I turn it off.

    I also found this link refering to the same problem:
    https://github.com/Microsoft/CodeContracts/issues/439