鲁棒性和语境代码验证

第一部分：稳健性检验

通过Anirban Gangopadhyay和Ram Cherukuri

这是第一部分两部分系列概述代码验证方法。

我们一开始就有一个问题：在什么阶段的软件开发我要验证我的代码？

答案很简单。你应该确认它在你编译好之后，当代码是新鲜的在你的脑海。一旦你出潜在的错误，审查和修正这些错误可能是几乎微不足道。修正错误永远不会在工作流程阶段之后更容易。

如果按照这个方法，你最有可能验证的代码单元。所述单元可能会被在开发周期以后集成到现有的代码库。Polyspace^®s manbetx 845产品让你实现你的验证两种不同的方式：通过稳健性验证，在验证你在隔离的单元，或通过上下文的验证，在您确认您的单位在剩下的代码库的情况下。在接下来的两个职位，我们提供一些指引，这将有助于你决定采取哪一种方法。

但首先，有什么区别呢每种方法化妆？让我们开始与稳健性检验。

在稳健性检验，Polyspace产品验证您的单位是稳健的（即，它是对某些错误s manbetx 845对所有输入，未定义函数，函数调用序列是安全的）。如果按照这个办法，没有新的错误应该代码集成和测试过程中出现。如果你查看并修正所有错误标记由Polyspace产品，您不必再审查单位（文件或功能）。s manbetx 845

让我们举例说明，几个简单的例子此行为。

可以有效抵抗所有输入

在这个例子中，NUM1和NUM2是函数的输入dividebydifference。除了它们的数据类型，Polyspace不能确定什么对NUM1和NUM2从这个代码。因此，它认为在的范围内的所有可能的值INT变量：

• 操作的结果NUM1 - NUM2和NUM / DEN可以超过允许的值INT变量。因此，Polyspace发出警告可能的溢出在这两种操作。
• NUM1可以等于NUM2。因此，Polyspace发出警告零潜在的分裂错误的划分。

然而，一旦Polyspace产品指出了你的代码的s manbetx 845漏洞，就可以使我们的函数采取适当行动更加稳健。例如，在上面的例子中，您可以将检查由零，以防止溢出和分裂。

可以有效抵抗所有未定义功能

假设你的代码的单位来电外部函数的单位和/或你不具备的功能定义。你怎么能保证自己，一旦函数定义不会在你的代码中出现一个新的运行时错误？您可以使用鲁棒性的方法。

在上面的例子中，巢穴被声明期间1和3之间分配一个值。然而，它的地址传给checkDenominator。巢穴有可能改变checkDenominator。自定义checkDenominator不提供，Polyspace产品考虑的可能性，s manbetx 845巢穴是可以改变的，并且可以具有在一个范围内的任何值INT变量。因此，它警告说，师可能零错误导致分裂。

然而，一旦Polyspace产品指出这个错误，你s manbetx 845可以保护部门，例如，通过传球巢穴至checkDenominator通过值，而不是通过一个指针。现在，除法运算是安全的，无论什么定义checkDenominator可能。

鲁棒性验证还从用户的角度来看吸引力。验证使用这种方法的设置，需要较少的努力。您提供源文件和目标设置后，你可以继续运行验证。默认设置的目的是验证你的代码对所有输入，函数定义，等等。

因此，稳健性检验是要走的路，不是吗？嗯......在实践中，你必须权衡花在与花审查显著更高一些错误的时间设置的时间。然而，使用鲁棒性的做法可能会导致审核太多的潜在的错误。

为了发现鲁棒性验证过程中的所有错误，Polyspace产品做出未知数如输入变量广泛的假设。s manbetx 845涉及那些未知的大多数操作都可能会失败。因此，您可以查看比你的时间允许更多的潜在的错误。

接下来的文章示出了替代验证方法（称为上下文代码验证），其解决了这个问题。