代码之家 › 专栏 › 技术社区 › Judah Gabriel Himango

codecontracts-误报

code-contracts c#

5

Judah Gabriel Himango · 技术社区 · 14 年前

我刚开始在一个现有的中型项目上在.NET 4中试验codecontracts,我很惊讶静态检查器向我发出了关于以下代码段的编译时警告:

public class Foo
{
   private readonly List<string> strs = new List<string>();

   public void DoSomething()
   {
       // Compiler warning from the static checker:
       // "requires unproven: source != null"
       strs.Add("hello");
   }
}

为什么codecontracts静态检查器抱怨strs.add(…)行?strs不可能是空的,对吧?我做错什么了吗?

4 回复 | 直到 14 年前

1

8

Rich 14 年前

该字段可以标记 readonly 但不幸的是,静态检查器不够智能。因此,由于静态检查器不能自己推断 strs 从不为空,必须通过不变量显式地告诉它:

[ContractInvariantMethod]
private void ObjectInvariant() {
    Contract.Invariant(strs != null);
}

2

3

Gabe Timothy Khouri 14 年前

下面是有效的代码,我希望生成警告。

public class Foo 
{ 
   private readonly List<string> strs = new List<string>(); 

   public Foo()
   {
       // strs is readonly, so we can assign it here but nowhere else
       strs = ResultOfSomeFunction();
   }

   public void DoSomething() 
   { 
       // Compiler warning from the static checker: 
       // "requires unproven: source != null" 
       strs.Add("hello"); 
   } 
}

很有可能,他们的分析器不会确保构造函数中没有任何内容可以更改 strs . 或者你正在改变 STRS 在一个构造器中,你没有意识到。

3

1

Peli 14 年前

小更正:Pex使用Z3,一个SMT解算器,而Clousot(静态检查器代码名)使用抽象解释和抽象域。

4

0

Jörg W Mittag 14 年前

我对.NET对象初始化语义的复杂性还不够了解,无法回答您的直接问题。但是,这里有两个提示:

Microsoft Research's Pex 可以自动生成单元测试,精确地证明在什么条件下可能会发生违反合同的情况。它和CC使用相同的定理证明器和静态分析器,所以这是一个公平的赌注,两者都同意。
证明合同等同于解决中止问题,所以仅仅因为CC不能证明那是不可能的 null 不代表不是真的。IOW:CC可能是错误的,你需要帮助它和 Contract.Assume (或者,如果你有信心, Contract.Assert )

有趣的是,如果您显式地添加对象不变量断言, strs 绝不可能 无效的 CC 是能够证明那个因此,也可以证明 strs.Add() 永远不会是空引用:

[ContractInvariantMethod]
private void StrsIsNotNull()
{
    Contract.Invariant(strs != null);
}

所以,我想我的直觉是正确的:在这种情况下,CC是完全错误的。(或者更准确地说:将C的语义编码到定理证明器中是不完整的。)