静态检查器和int.maxvalue [英] static checker and int.maxvalue

问题描述

我有以下方法：

public int Add(int a, int b)
        {
            IsNat(a, b);
            ResultIsNat();  // not true for 1 + int.MaxValue, but static analyzer does not catch it..
            Contract.Ensures(Contract.Result<int>() == a + b);

            return a + b;
        }

[ContractAbbreviator]
        public void IsNat(int a, int b)
        {
            Contract.Requires(a >= 0);
            Contract.Requires(b >= 0);
        }

        [ContractAbbreviator]
        public void ResultIsNat()
        {
            Contract.Ensures(Contract.Result<int>() >= 0);
        }

静态分析器无法捕获有问题的Add（1，int.MaxValue）。所以我猜静态分析器没有模型溢出？

The static analyzer doesn't catch the problematic Add(1, int.MaxValue). So I guess the static analyzer doesn't model overflow?

谢谢。

推荐答案

静态检查器在每次操作后都假设在评估此类操作时没有发生溢出。

The static checker assumes, after each operation that no overflow has happened in the evaluation of such an operation.

这是为了减少警告和合同（许多）你必须编写以消除这些警告。

This is to reduce the number of warnings, and of contracts (many many) that you have to write to get rid of those warnings.

如果检查溢出对你很重要，那么用/ checked编译或使用checked关键字。

If checking overflows are important for you, then compile with /checked or use the checked keyword.

然后，添加选项-arithmetics：obl = arithmeticoverflow。

Then, add the option -arithmetics:obl=arithmeticoverflow.

在这种情况下，分析仪会发出警告。

In this case the analyzer will emit a warning.

ciao

f

这篇关于静态检查器和int.maxvalue的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！