代码契约静态分析仪无法检测琐碎违反合同

我有这样的代码：代码契约静态分析仪无法检测琐碎违反合同

using System; 
using System.Diagnostics.Contracts; 

namespace TestCodeContracts 
{ 
    class Program 
    { 
     public static int Divide(int numerator, int denominator, out int remainder) 
     { 
      Contract.Requires<ArgumentException>(denominator != 0); 
      Contract.Requires<ArgumentException>(numerator != int.MinValue || denominator != -1, "Overflow"); 
      Contract.Ensures(Contract.Result<int>() == numerator/denominator); 
      Contract.Ensures(Contract.ValueAtReturn<int>(out remainder) == numerator % denominator); 

      remainder = numerator % denominator; 
      return numerator/denominator; 
     } 

     static void Main(string[] args) 
     { 
      int remainder; 
      Console.WriteLine(Divide(10, 6, out remainder)); 
      Console.WriteLine(Divide(5, remainder, out remainder)); 

      Console.WriteLine(Divide(3, 0, out remainder)); 

      Console.Read(); 
     } 
    } 
}

在第一鸿沟电话，如果我通过0更换6，那么静态分析正确地警告反对。

如果我将6替换为5，则我（正确）在第二次除法调用时发出警告。

但是，无论如何，我从来没有得到任何警告在第三次分割呼叫。相反，我只是得到一个运行时错误。

为什么静态分析仪无法检测到第三行是合同违规？

我在Windows 8 64位上使用Visual Studio 2012。代码合同是Microsoft Code Contracts (devlabs_TS) 1.4.51019.0 for .NET（这似乎是截至2012年12月的最新版本）。

来源

2012-12-08 luiscubal

你是否仔细检查了这个？重建之间？它可以更好地设置更多的测试调用（而不是改变6到0的方法）。 –

@HenkHolterman重建不会改变我的结果。此外，如果我在三个测试函数（'Test1'，'Test2'和'Test3'）中隔离我的三种情况（第一次除法调用的'6'，'5'和'0），然后调用三个测试函数中，我只在两个测试函数中发出警告 - 每个测试函数的第三次除法调用都不会收到警告，即使它明显违反合同。 – luiscubal

我贴this in the code contracts forum。确认这确实是一个错误，它会被修复。

的错误是，静态验证认为，除（3,0 ......）不可达

（...）

我们将修复的bug。

来源

2012-12-13 11:48:56 luiscubal

这是一个有趣的问题。

我终于简化Divide下到这一点：

public static int Divide(int numerator, int denominator) 
{ 
    Contract.Requires<ArgumentException>(denominator != 0); 
    return numerator/denominator; 
}

这引发了正确的警告：

static void Main(string[] args) 
{ 
    Console.WriteLine(Divide(10, 10)); 
    Console.WriteLine(Divide(10, 0)); 
}

需要注意的是，我发现你有一般重建，而不是建立，即使只有一个项目。必须有重建时清理的代码合同文物。

这并不抛出警告：

static void Main(string[] args) 
{ 
    Console.WriteLine(Divide(10, 9)); 
    Console.WriteLine(Divide(10, 0)); 
}

我可以触发警告的唯一途径是，如果第一个鸿沟分母为10（这显然也是工作时，它为0）。

它看起来像一个错误 - 我会发送一封电子邮件给代码合同团队，看看他们说什么。

来源

2012-12-10 02:00:45 Mightymuke

你的意思是“你必须重建而不是建造”。你的意思是“你必须为了使它正常工作”或“你必须为了重现这种行为”？我无法重现这一点'分而治之（10，9）' - 在这种情况下，我仍然会收到警告。无论哪种方式，我没有发送电子邮件，但我发布在他们的论坛 - http://social.msdn.microsoft.com/Forums/en-US/codecontracts/thread/85473b0a-ea63-45f9-841e-6912c58621a9 – luiscubal

为了使代码合同正常工作，我必须重新编译。 – Mightymuke

代码契约静态分析仪无法检测琐碎违反合同

回答

相关问题