Why contract is malformed when using default(Type)?

Question

Hi,

When compiling code which uses code contracts, I have a very strange error I don't understand.

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(
        this.isSubsidiary ||
        this.parentCompanyId == default(Guid));
}

fails with the following error:

Malformed contract. Found Invariant after assignment in method '<ProjectName>.ObjectInvariant'.

If the code is modified like this:

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(
        this.isSubsidiary ||
        this.parentCompanyId == Guid.Empty);
        // Noticed the Guid.Empty instead of default(Guid)?
}

it compiles well.

What's wrong with my default(Guid)?

Answer 1

The IL generated for this:

Console.WriteLine("{0}, {1}", default(Guid), Guid.Empty);

is:

    .locals init (
        [0] valuetype [mscorlib]System.Guid CS$0$0000)
    L_0000: nop 
    L_0001: ldstr "{0}, {1}"
    L_0006: ldloca.s CS$0$0000
    L_0008: initobj [mscorlib]System.Guid
    L_000e: ldloc.0 
    L_000f: box [mscorlib]System.Guid
    L_0014: ldsfld valuetype [mscorlib]System.Guid [mscorlib]System.Guid::Empty
    L_0019: box [mscorlib]System.Guid
    L_001e: call void [mscorlib]System.Console::WriteLine(string, object, object)

Which corresponds to something like:

Guid CS$0$0000 = new Guid();
Console.WriteLine("{0}, {1}", CS$0$0000, Guid.Empty);

Code Contracts works directly on the IL, so it thinks you've written something like the second version. The rewriter is saying you're not allowed to assign to variables before the contracts, so it gives an error.

However, this is weird, because while this doesn't work:

var x = new Guid();
Contract.Invariant(
    this.isSubsidiary ||
    this.parentCompanyId == x);

this does, but it is clearly an "assignment before Invariant"!

var x = Guid.Empty;
Contract.Invariant(
    this.isSubsidiary ||
    this.parentCompanyId == x);

I think they actually modified the checker to allow some assignments like this (for ease of use), but that they haven't allowed all cases... whether this is intended or not is beyond my knowledge.

I'd report this on the Code Contracts forum, it may be a bug.