CODEWITHSUNDEEP
c#code-contracts
Pavel Voronin
Pavel Voronin

Reputation: 14015

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);

Upvotes: 2

Views: 221

Answers (2)

Alex Filipovici
Alex Filipovici

Reputation: 32571

You might want to re-check the following check box and then, rebuild the project:

right click on the project -> Properties -> Code Contracts -> Show squigglies

Also, make sure that your solution's Active Config (or the specific project's Build configuration) matches the Configuration from the Code Contracts property page.

Upvotes: 1

Daniel Hilgarth
Daniel Hilgarth

Reputation: 174457

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.

Upvotes: 2

Related Questions