Search code examples
c#code-contracts

Is static checking performed for Contract.Ensures?

I cannot understand why static checker says that everything is ok for this method:

public static int GetNonNegativeValue()
{
    Contract.Ensures(Contract.Result<int>() >= 0);

    return -1;
}

Static checking is on.

Update:

this is also ok. 

var i = Doer.GetNonNegativeValue();
Contract.Assert(i < 0);
Solution

  • It seems as if this warning disappears when you activate "Infer Requires" in the settings of the static checker.

    It will than infer Contract.Requires(false) ("CodeContracts: Suggested requires: Contract.Requires(false);") which will make this method "invalid", as it now can't be called without raising a contract exception. It looks like the contract checker doesn't verify the Ensures on such a method, because it wouldn't execute the return statement anyway.

    BTW: Activating or deactivating "Show squigglies" doesn't change this behaviour in any way. I can only assume that the OP didn't just change this setting when he tested it.