Coverity 无法报告无限循环缺陷

Question

如果我传入值为 0 的除数，我有以下 Java 代码可能会无限循环。但 Coverity 无法为我报告此错误。

class InfinityLoopExample {
  public int div(final int dividend, final int divisor)  {
    int ret = 0;
    int x = dividend;
    while (x > divisor) {
      x = x - divisor;
      ret++;
    }
    return ret;
  }
}

//And following code to actually call that method i.e. in main.
//This will make sure infinite loop real happens
final InfinityLoopExample infinityLoopExample = new InfinityLoopExample();
final int ret1 = infinityLoopExample.div(3,0);
System.out.println("infinityLoopExample.div:" + ret1);

从下面的 coverity link 可以清楚地看出 coverity 可以在其静态代码分析期间报告此类错误： https://cwe.mitre.org/data/definitions/835.html

我运行覆盖代码扫描上面Java代码，它不能报告无限循环问题。有没有人运行 coverity code scan against Java project can give some light？

P.S 我有大小为 151K 的覆盖构建日志文件。如果需要，我可以 post。

Answer 1

作为最初设计 INFINITE_LOOP 检查器的两个人之一，我在 2010 年左右为 Coverity 工作时（我现在不在了），我可以说说为什么这可能不会被报道，虽然我不能详细介绍，因为这属于 Coverity（现在是 Synopsys）的专有知识属性.

首先，必须认识到 Coverity 不会报告任何给定缺陷类型的所有实例。这与 halting problem 的不可判定性有关；完全准确的全自动静态分析在数学上是不可能的。此外，大多数 Coverity 检查器旨在报告不超过 20% 的误报，为了做到这一点，它要求代码在愿意报告之前包含相当有力的问题证据。

函数 div 没有包含足够有力的问题证据，因为 divisor 永远不应该作为零传入是合理的。相反，如果它包含类似 if (divisor==0) {...} 的内容，那么将成为应该容忍零参数的有力证据。当然，这不是该工具识别的唯一证据。如果您添加了这样的代码，包含逻辑内部矛盾的明确证据，并且检查器 still 没有报告，那么我建议将示例报告给 Coverity 支持团队。

现在，除了 div，您的示例还包括一个调用站点：

final int ret1 = infinityLoopExample.div(3,0);

据此，divisor显然可以为零，对吧？是的——但现在您可能运行进入了这个特定检查器的限制。

让我们暂时转移一下，与另一个检查器 FORWARD_NULL 进行比较，后者是负责报告 null 取消引用问题的主要检查器。 FORWARD_NULL 不会报告这个：

int deref(MyClass c) { return c.someField; }

如果 c 为 null，方法 deref 将抛出 NullPointerException，但我们没有证据表明 c 曾经为 null。然而，FORWARD_NULL 认识到了潜力，所以它记得 deref 无条件取消引用它的论点。稍后如果它看到这样的呼叫站点：

deref(null);

然后它将报告该呼叫站点。

但是，INFINITE_LOOP 没有，或者至少在最初设计时没有，具有可比较的机制。如果它找不到足够的理由来报告包含函数内的循环，那么它不会报告，无论调用站点可能发生什么。

以这种方式向 Coverity 团队提出增强请求以扩展 INFINITE_LOOP 的检测能力并不是没有道理的。但是，如果您这样做，我强烈建议您提交调用代码更真实的代码。 Coverity 是否遗漏了实际生产代码中的真正缺陷？提交那个。 Coverity 设计理念的另一个要素是强调真实代码的准确性，而不是人为的示例，因为两者有许多重要的差异，分析对这些差异非常敏感。

Coverity 无法报告无限循环缺陷

Coverity can't report infinite loop defect

java

coverity