gpt4 book ai didi

c# - Code Contracts 静态分析器不检测琐碎的契约(Contract)违规

转载 作者:行者123 更新时间:2023-11-30 21:01:55 26 4
gpt4 key购买 nike

我有这个代码:

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();
}
}
}

在第一次调用 Divide 时,如果我用 0 替换 6,那么静态分析会正确地发出警告。

如果我用 5 替换 6,那么我(正确地)在第二次 Divide 调用时收到警告。

但是,无论如何,我从未在第三次 Divide 调用中收到任何警告。相反,我只是收到一个运行时错误。

为什么静态分析器检测不到第三行是违约?

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

最佳答案

我发布了 this in the code contracts forum .确认这确实是一个错误,并且会修复它。

The bug is that the static verifier thinks that the Divide(3, 0... ) is unreachable

(...)

We will fix the bug.

关于c# - Code Contracts 静态分析器不检测琐碎的契约(Contract)违规,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/13777708/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com