broken StaticChecker for nullable types. No fix after 3 years!

Question

public static int? Foo(int? bar)
{
    Contract.Requires(bar.HasValue); // works
    Contract.Requires(bar > 5); // unproven warnings no matter what

This has been posted several times over the years now and it is still broken.

http://social.msdn.microsoft.com/Forums/en-US/codecontracts/thread/7cde2d65-1009-4e3b-8e8d-f2388a7d75ec

This can't be that difficult to fix.

When can we finally expect a fix for that?

I just come from from a project where I had to work with IE7 and really guys I am tired of Microsoft software shipped broken and never fixed.

Answer 1

Do you get warnings if you use bar.Value instead of bar?

(Actually, I'm surprised you can write bar > 5 and get a bool out instead of a nullable bool. Is null > 5?)

Answer 2

I just come from from a project where I had to work with IE7 and really guys I am tired of Microsoft software shipped broken and never fixed.

You realise that the Code Contracts stuff is prototype and not officially released, right? It has NOT shipped!

See the "about" notes for DevLabs:

Here Microsoft teams are reaching out to broad developer audiences with new, developer-focused technologies well before they are officially released. Our goal is that many of these technologies will eventually be incorporated into Microsoft products in some form or another. Others may be retired or released into the shared-source community. Some projects highlighted here are already in a released state but they have new concepts within them that we are trying out, to see how developers react to them for possible inclusion in other Microsoft products. Some are in prototype packages that will evolve into larger, well known products.

By and large, the prototypes hosted here are just that—prototypes. They are developed by teams of Microsoft employees looking at eventually merging each technology into a product, but they are mostly in very early stages. So they won’t all work perfectly, and they won’t be hosted here forever. Please play with them, stress them, tell us what you think, but do not use them in production scenarios at this time.

Answer 3

Do you get warnings if you use bar.Value instead of bar?

(Actually, I'm surprised you can write bar > 5 and get a bool out instead of a nullable bool. Is null > 5?)

No. You can use whatever you can imagine. You can't even suppress the warning.

int? i = 9;
Contract.Assume(i.HasValue && i.Value > 0);
Foo(i);

public static int? Foo(int? bar)
{
     Contract.Requires(bar.HasValue);
     Contract.Requires(bar > 0);
     Contract.Requires(bar == null || bar > 0);
     Contract.Requires(!bar.HasValue || bar.Value > 0);

Answer 4

You realise that the Code Contracts stuff is prototype and not officially released, right? It has NOT shipped!

Then how come this is part of .Net Framework 4? Do you know of anything else in .Net Framework that is considered prototype? And even then, they had 3 years to fix a bug I found after playing 10 minutes with code contracts.

And if I remember correctly this feature was previously reserved to VS Ultimate Edition. Doing so Microsoft is saying that the static checker feature was worth to pay 12.000 USD. If you are correct that would mean they told us to pay 12.000 bucks for unsupported prototype software.

Answer 5

Why are you passing a nullable value into a method but requiring that it be non-null in the first place? Just take a normal integer parameter.

I don't get a warning when verifying that code, and I have warnings set to high and all the implicit obligations turned on.

        static void Main(string[] args) {
            int? i = 9;
            Foo(i);
        }
        public static int? Foo(int? bar) {
            Contract.Requires(bar.HasValue);
            Contract.Requires(bar > 0);
            return bar;
        }

If I change 'bar > 0' to 'bar != 9' I do get a warning, meaning the static verifier understands nullable types in this particular situation. Are you at least using the most recent version?

Answer 6

You realise that the Code Contracts stuff is prototype and not officially released, right? It has NOT shipped!

Then how come this is part of .Net Framework 4? Do you know of anything else in .Net Framework that is considered prototype? And even then, they had 3 years to fix a bug I found after playing 10 minutes with code contracts.

And if I remember correctly this feature was previously reserved to VS Ultimate Edition. Doing so Microsoft is saying that the static checker feature was worth to pay 12.000 USD. If you are correct that would mean they told us to pay 12.000 bucks for unsupported prototype software.

Ah good point; I was just looking at the DevLabs FAQ.

Answer 7

If I change 'bar > 0' to 'bar != 9' I do get a warning, meaning the static verifier understands nullable types in this particular situation. Are you at least using the most recent version?

Very odd. I copy paste your code and get the warnings.

The installer says (devlabs_TS) 1.4.50327.0 for .NET..  Microsoft.Contracts.dll says version 1.0.0.0. but dates from 27th of march this year. It has 16384 bytes.

Answer 8

I also get the spurious incorrect warning. I have installed the latest Code Contracts and enabled all the implicit non-null obligations.

Answer 9

The warning is only shown when setting the warning level to "hi".

I believe the problem is that the contract currently looks like this:

public Nullable(T value)
{
    Contract.Ensures(Contract.ValueAtReturn<T?>(out this).HasValue, null, "Contract.ValueAtReturn(out this).HasValue");
}

But shouldn't it look like this?:

public Nullable(T value)
{
    Contract.Ensures(Contract.ValueAtReturn<T?>(out this).HasValue, null, "Contract.ValueAtReturn(out this).HasValue");
    Contract.Ensures(Contract.ValueAtReturn<T?>(out this).Value == value, null, "Contract.ValueAtReturn<T?>(out this).Value == value");
}

Same with this operator (current version):

public static implicit operator T?(T value)
{
    T? nullable2;
    Contract.Ensures(Contract.Result<T?>().HasValue, null, "Contract.Result<T?>().HasValue");
    return nullable2;
}

And the second operator has no contract at all:

public static explicit operator T(T? value)
{
    T local2;
    return local2;
}

Should look this I guess:

public static explicit operator T(T? value)
{
    T local2;
    Contract.Requires(value.HasValue, null, "HasValue");
    Contract.Ensures(Contract.Result<T>() == value.Value);
    return local2;
}

Answer 10

The warning is only shown when setting the warning level to "hi".

I believe the problem is that the contract currently looks like this:

With level set to low, the error does not pop up. But then I can do this also without getting any warning:

static void Main(string[] args)
{
    int? i = -1;
    Foo(i);
}
public static int? Foo(int? bar)
{
    Contract.Requires(bar.HasValue);
    Contract.Requires(bar > 0);
    return bar;
}

What code are you referring to? CodeContract source?

Answer 11

The code is extracted from the installed code contracts (c:\Program Files (x86)\Microsoft\Contracts\Contracts\.NETFramework\v4.0\).
I used .NET Reflector to investigate them.

Perhaps there is a problem with the warning level and Nullable types, and warnings are shown only on "hi".

Answer 12

Hi, do you know if it's been fixed???