2

私はこのコードを持っています:

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 呼び出しで、 で置き換えると6、0静的分析はそれに対して正しく警告します。

で置き換える6と5、(正しく) 2 回目の Divide 呼び出しで警告が表示されます。

ただし、何があっても、3 回目の Divide 呼び出しで警告が表示されることはありません。代わりに、実行時エラーが発生します。

静的アナライザーが 3 行目が契約違反であることを検出できないのはなぜですか?

Windows 8 64 ビットで Visual Studio 2012 を使用しています。コード コントラクトはMicrosoft Code Contracts (devlabs_TS) 1.4.51019.0 for .NET(2012 年 12 月現在の最新バージョンのようです) です。

4

2 に答える 2

3

これをコード契約フォーラムに投稿しました。これは実際にバグであり、修正されることが確認されています。

バグは、静的ベリファイアが Divide(3, 0... ) に到達できないと判断することです。

(...)

バグを修正いたします。

于 2012-12-13T11:48:56.593 に答える
1

これは興味深い問題です。

私は最終的にこれに単純化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));
}

プロジェクトが 1 つしかない場合でも、通常はビルドではなくリビルドする必要があることに注意してください。再構築時にクリーンアップされるコード コントラクト アーティファクトが存在する必要があります。

これは警告をスローしません：

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

警告をトリガーできる唯一の方法は、最初の除算の分母が 10 の場合でした (0 の場合も明らかに機能しました)。

バグのように思えます。コード コントラクト チームに電子メールを送信して、彼らの意見を確認します。

于 2012-12-10T02:00:45.767 に答える