标签: code-contracts

我正在使用CodeContracts静态分析工具.

我的代码:

截图http://i40.tinypic.com/r91zq9.png

(ASCII版)

该工具告诉我,这instance.bar可能是一个空引用.我相信相反.

谁是对的？我怎么能证明它错了？

我最近迁移了许多手动前提条件测试和代码合同的异常抛出.而不是升级到.NET 4,我一直在使用Microsoft.Contracts.dll程序集,所以我可以坚持使用.NET 3.5(这是一个由.NET 3.5和.NET 4程序集使用的库).我在Visual Studio 2010中设置了合同重写器,合同工作正常.

但是,因为我已经完成了那个开关,所以我注意到调试器在带有契约的方法中表现得很有趣,特别是在具有ContractInvariantMethod的类中.执行游标似乎并不总是与突出显示的行匹配,一些断点无法被命中,我有一个方法,调试器无法告诉本地变量名称,并显示类似的东西CS$1$0000.这是在调试版本中.

Microsoft.Contracts.dll在.NET 3.5到VS10中使用代码契约是否存在已知问题？.NET 4中的代码合同是否会出现类似的问题？

[编辑]这个问题让我在Microsoft Connect上创建了一个错误:https://connect.microsoft.com/VisualStudio/feedback/details/573983/code-contract-rewriting-messes-up-local-variable-names-in -迭代器的方法,同时调试

我写的一个课程实现IDictionary<string, object>.在我的CopyTo实现中,我想使用代码契约:像Contract.Requires<ArgumentNullException>(array != null).

但是,我收到此警告(为了便于阅读,删除了一些名称空间):

方法' LuaDictionary.CopyTo(KeyValuePair<String,Object>[],Int32)'实现接口方法' ICollection<KeyValuePair<String,Object>>.CopyTo(KeyValuePair<String,Object>[],Int32)',因此无法添加Requires.

我看到有一些相关的问题,但它们似乎都与用户控制下的接口有关.显然,IDictionary<T, U>不在我的控制之下,所以我不能用它ContractClassFor或类似的东西注释它.

我在这里无法使用代码合同吗？如果是这样......主要的无赖......

我试图通过代码契约获得VS2010 Ultimate以生成错误而不是警告.

我有这个简单的测试程序:

using System.Diagnostics.Contracts;

namespace MyError
{
  public class Program 
  {
     static void Main(string[] args)
     {
         Program prog = new Program();
         prog.Log(null);
     }

     public void Log(string msg)
     {
         Contract.Requires(msg != null);
     }
  }
}

它正确地确定违反了合同:

C:\...\Program.cs(10,13): warning : CodeContracts: requires is false: msg != null

在我的csproj文件中有Debug的这个属性字段:

TreatWarningsAsErrors>true

我是否还需要在项目设置中设置其他内容才能将这些内容变为错误？

我无法在课堂上配置代码合同.我已经按照文档和示例,但它不起作用.

我想将Code Contracts条件插入我的界面,这里是我的代码

界面

 [ContractClass(typeof(ArticleBLLContract))]
 public interface IArticleBLL
 {
    int getArticleNSheet(string IdBox);
    IEnumerable<IArticle> getArticleValue(string IdBox, string IdLanguage);
}

合同类

[ContractClassFor(typeof(IArticleBLL))]
public sealed class ArticleBLLContract : IArticleBLL
{
    int IArticleBLL.getArticleNSheet(string IdBox)
    {
        Contract.Requires<ArgumentOutOfRangeException>(!String.IsNullOrEmpty(IdBox),"IdBox has no valid value");                        

        return default(int);
    }

    IEnumerable<Base.Article.IArticle> IArticleBLL.getArticleValue(string IdBox, string IdLanguage)
    {
        Contract.Requires<ArgumentOutOfRangeException>(!String.IsNullOrEmpty(IdBox), "IdBox has no valid value");
        Contract.Requires<ArgumentOutOfRangeException>(!String.IsNullOrEmpty(IdLanguage), "IdLanguagehas no valid value");

        Contract.Ensures(Contract.Result<IEnumerable<Base.Article.IArticle>>() != null, "Return value is out of Range");

        return default(IEnumerable<Base.Article.IArticle>);
    }        
}

申请合同的班级

public class ArticleBLL : IArticleBLL
{

    public int getArticlNSheet(string IdBox) …

鉴于以下示例代码,我如何配置Pex以尊重我的代码合同？

    public static IEnumerable<User> Administrators(this UserGroup userGroup)
    {
        Contract.Requires(userGroup != null);
        Contract.Requires(userGroup.UserList != null);

        return userGroup.UserList.Where(ul => ul.IsAdmin == true);
    }

当前问题:当我运行Pex时,它仍然会生成违反指定代码契约的测试用例.

仅供参考:以下是我的csproj文件中的"代码合同"设置.

编辑:在SP1中有什么破坏？

• 我正在使用Code Contracts ver:1.4.40602.0
• 我复制了必要的内容和转换文件
• Sandcastle根据我的合同要求输出例外情况

示例代码:

public class MyClass
{
    public MyClass(Object obj)
    {
        Contract.Requires<ArgumentNullException>(obj != null);
    }
}

结果输出(在我的文档中):

| Exception                       | Condition                       |
|---------------------------------|---------------------------------|
| System.ArgumentNullException    | obj == null                     |

这并不是那么糟糕,但我想知道是否有办法自定义条件的文本？我试图添加用户消息Contract.Requires<ArgumentNullException>(obj != null, "obj is null.");,但这并没有解决任何问题.

在过去,我必须为异常编写自己的xml文档部分.我是否必须再次这样做以获得我需要的东西？

免责声明:由于Code Contracts(目前)是一个DevLabs项目,这可能会改变,但我想知道它现在是否已经可用......如果没有,我一定会建议它.

我正在尝试lock使用以下示例来研究.NET Code Contracts如何与关键字进行交互:

public class TestClass
{
  private object o1 = new object();
  private object o2 = new object();

  private void Test()
  {
    Contract.Requires(this.o1 != null);
    Contract.Requires(this.o2 != null);
    Contract.Ensures(this.o1 != null);

    lock (this.o2) {
      this.o1 = new object();
    }
  }
}

当我运行代码契约静态分析工具时,它会打印一个警告: Ensures unproven: this.o1 != null

如果我做了以下任何一项:

• 改变o2在lock给o1,
• o1将lock块内部更改为o2,
• 在lock块内添加第二行,分配new object给o2
• 更改lock (this.o2)到if (this.o2 != null), …

我有以下软件:

• Visual Studio 2013 Update 2
• 代码合约(1.6.60617.15)
• ReSharper C#版(8.2.0.2160)
• ReSharper代码合同(1.0.0.0)

当我用代码契约打开一个方法时,ReSharper对合同感到困惑:

它警告我chapter可以为空,即使合同要求它不是.也:

合同不变方法被标记为never used.技术上是正确的,但它不应该告诉我,因为代码合同重写器使用该方法来获取有关每个不变量的信息.我如何教授ReSharper关于代码合同以纠正这两个问题？

请注意,这可能与此问题重复,我不完全确定.

我的问题是我有一个类库项目,它引用了第三方类型库(COM).我想将契约放入类库中的方法,如下所示:

public class foo
{
    public static int divide(TypeFromTypeLib tftl, int a, int b)
    {
        Contract.Requires<ArgumentException>(b != 0);
        return a / b;
    }
}

然后让客户项目使用这种方法,例如

var n = foo.divide(null, 4, 2);

但我也希望客户端项目在其某些方法中也使用契约.因此,我将两个项目的Code Contracts属性设置为'执行运行时合同检查'(没有它,您将获得运行时断言,告诉您它需要此设置).

现在,当我尝试编译客户端时,我收到以下错误:

无法解析成员引用:my_class_lib.foo::divide.

ccrewrite:error:由于元数据错误而重写中止.

这似乎是不可避免的 - 任何时候调用一个类型来自第三方类型库的方法.从方法的签名中删除类型,没关系.

谁能解释为什么会这样？这是一个线索,我的代码结构从根本上是有缺陷的(如果是,为什么？),或者它是代码合同的怪癖？是否有针对此问题的建议修复程序？