为什么使用default(Type)时合约格式错误？

Question

当编译使用代码契约的代码时，我遇到一个非常奇怪的错误，我不明白。

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

失败并出现以下错误：

合同格式错误。在方法“.ObjectInvariant”中赋值后发现 Invariant。

如果代码像这样修改：

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

它可以很好地编译。

我的 default(Guid) 有什么问题吗？

Answer 1

为此生成的 IL：

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

是：

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

对应于以下内容：

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

Code Contracts 直接在 IL 上工作，因此它认为您已经编写了类似于第二个版本的内容。重写者说你不允许在合同之前分配给变量，所以它给出了一个错误。

然而，这很奇怪，因为虽然这不起作用：

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

但它确实有效，但它显然是“不变式之前的赋值”！

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

我认为他们实际上修改了检查器以允许像这样的一些分配（为了便于使用），但他们并没有允许所有情况......无论这是有意还是无意超出了我的知识范围。

我会在代码契约论坛上报告此问题，它可能是漏洞。