False positive: precondition is redundant

Question

Why do I get the following warning for this trivial code sample as soon as the Warning Level is on the 2nd level or higher?

public int Foo(int a)
{
    if (a >= 0) throw new ArgumentException("a should be negative", "a");
    Contract.EndContractBlock();
    return a;
}

CodeContracts: Suggested requires: This precondition is redundant: Consider removing it. Are you comparing a struct value to null?

Clearly an integer can be negative so the precondition is hardly redundant, so why do I get this warning?

Edit: Here is what ILSpy shows for the created function when looking at the exe:

public int Foo(int a)
{
    if (a >= 0)
    {
        ContractHelper.RaiseContractFailedEvent(ContractFailureKind.Precondition, null, "a < 0", null);
        throw new ArgumentException("a should be negative", "a");
    }
    return a;
}

Code Contracts settings

@Lakshay Not at all in this cut down version. But removing it doesn't remove the suggestion. Just overlooked it when creating a minimal example, removed it. — Voo, Jun 18 '15 at 12:07
Are you sure this is the exact code? Could it be that the comparison is performed on an unsigned integer, for example? Can you check the IL this generates? — Luaan, Jun 18 '15 at 12:11
@Luaan I can copy the exact code shown here into my VS 2013 project with Code Contracts and receive that warning when building. Assembly Mode is "Custom Parameter Validation" which is needed when using the backcomp if-then-throw version of code contracts from what I understand (otherwise I get a warning about it not being supported without this mode and that it'll be handled like a Require). — Voo, Jun 18 '15 at 12:13
Does it happen when you do `0 <= a` ? `clt` is used for `as` and `is` normally in release mode. Can you check if it is different for release/debug too? — leppie, Jun 18 '15 at 12:21
On a sidenote: Shouldnt it be an ArgumentOutOfRangeException ? — CSharpie, Jun 18 '15 at 12:21
@leppie Doesn't change anything. The generated IL is `ldarg.1; ldc.i4.0; clt` for the first version (turned around and cgt for the second one) so nothing out of the ordinary I'd say. — Voo, Jun 18 '15 at 12:24
@Voo: The IL analyzer must have a bug IMO. To work around, check the sign bit or something. — leppie, Jun 18 '15 at 12:28
I don't get that warning. What are your code contracts settings, and what version are you using? (I'm using 1.7.11202.10) — Matthew Watson, Jun 18 '15 at 12:32
@Matthew Interesting, just downloaded the newest version today (seems to be the same) and running VS 2013 professional Update 4. Maybe I should create a new solution to see if that's the problem. In any case I added the screenshot from the code contracts settings page. Edit: Just remembered that I increased the Warning level a bit because I was playing with `Contract.Assert` earlier, so this probably has something to do with it. — Voo, Jun 18 '15 at 12:34
Which warning level? Are you getting this warning during static contract checking? Also, debug or release build? (I'm using same VS as you btw) — Matthew Watson, Jun 18 '15 at 12:38
@Matthew It's a debug build with any CPU, static contract checking, full runtime contract checking and "relevant warnings" (the second from the left). The image shows my exact settings that I use to get the error if you need more information. — Voo, Jun 18 '15 at 12:40
I also note that `Contract.Requires(a < 0);` doesn't give the warning. — Matthew Watson, Jun 18 '15 at 13:21
I think you should post this as an issue here: https://github.com/Microsoft/CodeContracts — Matthew Watson, Jun 18 '15 at 13:22
@Matthew Yep seems like a bug and not just a misconfiguration or misunderstanding on my part. Will do tonight (aka a few hours). Thanks for your help. — Voo, Jun 18 '15 at 14:04
[GitHub issue](https://github.com/Microsoft/CodeContracts/issues/67). — Voo, Jun 18 '15 at 19:09
My guess is that you are the victim of "Automatic Inference of Necessary Preconditions". Check section 6.6.4 of the code contracts reference manual titled "Inference". The a < 0 is probably being automatically propagated to callers, so spelling it out is redundant. — Mystra007, Jun 18 '15 at 20:41
For your reference the manual also says this about the Redundant Assumptions: Enabling this option causes the checker to attempt to prove the Contract.Assume statements and warn if they are provable. We suggest you use this option only occasionally to get rid of redundant assumptions, but not on a continuous basis, as it slows down the static analysis substantially." So my conclusion is that the options you have checked: infer requires and check redundant conditionals produces this warning because code contracts figured out the constraint... — Mystra007, Jun 18 '15 at 20:44
@Mystra Interesting idea, I'll check tomorrow. Weird that this is the default setting in VS then considering the given guidance. — Voo, Jun 18 '15 at 20:54

score 2 · Answer 1 · edited Jun 20 '20 at 09:12

I know this doesn't directly answer your question, but it appears you're using a legacy mode for Code Contracts.

This document describes the recommended assembly mode based on usage requirements:

http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf

From Pages 20, 21...

assembly mode usage guidelines

Another snippet from the document:

5.1.1 Assembly Mode

The contract tools need to know which usage mode you choose. If you use VisualStudio, select the Assemby Mode on the contract property pane as follows:

Usage 1 or 2: Standard Contract Requires

Usage 3: Custom Parameter Validation

This permits the tools to emit proper warnings when you violate the usage guidelines. If you use the tools from the command-line, pass the proper argument for the -assemblyMode option

So using "Standard Contract Requires" assembly mode you could do either of the following:

Contract.Requires<ArgumentException>(a < 0, "a");
// OR
Contract.Requires(a < 0, "a should be negative");

Neither of these generate any warnings for me.

I hope this helps anyway.

Cheers peteski

False positive: precondition is redundant

1 Answers1