为什么静态分析忽略double<;=并且>;=要求

本文关键字:并且 gt 要求 静态分析 double 为什么 lt | 更新日期: 2023-09-27 18:26:00

我有一个利用.NET代码契约的非常简单的类:

public class ContractSquareRoot
{
    /// <summary>
    /// Makes your life much easier by calling Math.Sqrt for you. Ain't that peachy.
    /// </summary>
    /// <param name="value">The value to calculate the square root from. No negatives!</param>
    /// <returns>The square root of the given value. Obviously always > 0.</returns>
    public double CalculateSquareRoot(double value)
    {
        Contract.Requires<ArgumentException>(0 <= value);
        Contract.Ensures(0 <= Contract.Result<double>());
        double squareRoot = Math.Sqrt(value);
        return squareRoot;
    }
}

当我调用具有负值的方法时,我希望静态代码分析会对此发出警告

class Program
{
    static void Main(string[] args)
    {
        var barMansSquareroot = new ContractSquareRoot();
        // This should not be possible...
        barMansSquareroot.CalculateSquareRoot(-42);
    }
}

但是,即使Contract.Requires未能抛出所需的异常,静态代码分析也会将每个断言标记为正确的。有趣的是,当我将值的类型更改为int或将<=替换为<时,它会警告我违规。不当行为仅限于doublefloat。我认为这与浮点值的精度有关。

当我制定这样的要求时,它甚至起作用:

Contract.Requires<ArgumentException>(!(0 > value));

那是个bug还是我做错了什么?

为什么静态分析忽略double<;=并且>;=要求

我希望您可能会错过安装Microsoft代码合约。

您可以从Microsoft Research下载Microsoft代码合同:http://research.microsoft.com/en-us/projects/contracts/

现在,在您的项目属性上,您将获得一个额外的选项卡,可以在其中设置运行时和静态检查。