java - 使用 Java Checker Framework 的 Nullness Checker 注释可重入性

Question

我正在尝试Checker Framework使用 Java 8 的 Nullness 检查器。当我在以下代码上运行检查器时:

import java.util.HashMap;
import java.util.Map;

import org.checkerframework.checker.nullness.qual.Nullable;

class A {
    public void f() {}
}

public class Foo {
    private Map<A,Integer> map = new HashMap<>();
    private @Nullable A x;

    public void setX(@Nullable A x) {
        this.x = x;
    }

    public void call() {
        if (x != null) {
            map.put(x, 0);
            x.f();
        }
    }
}

检查器对x.f();发出警告:取消引用可能的空引用x。这当然是有道理的。 Checker Framework 不知道 map.put 的作用。 map 对象可能已经拥有对 this 的引用，然后对其调用 setX(null) 。

现在我的问题如下。有没有办法告诉 Checker 框架，方法不会修改除调用它的对象之外的任何对象？因为map.put没有调用setX方法，所以x的值不会改变。

要消除警告，我可以将调用方法更改为:

public void call() {
    A y = x;
    if (y != null) {
        map.put(y, 0);
        y.f();
    }
}

现在没有警告。这也是有道理的:局部变量不能从外部访问。但我不喜欢引入这个局部变量的唯一目的是消除警告。

或者，我可以通过 @MonotonicNonNull 注释字段 x。但在我的实际用例中，我希望保留将该字段设置为 null 的可能性。

提前致谢!

Answer 1

您的问题已经提供了几种抑制警告的绝佳方法，因此您清楚地知道自己在做什么。

但是，您想要更好的方法。您想知道如何使 Checker Framework 从一开始就不会发出警告。您的关键问题是:

Is there any way to tell the Checker Framework that a method does not modify any object other than the object it's called on?

不幸的是，Checker Framework 目前不具备此功能。 Manual section 21.4.3, "Side effects, determinism, purity, and flow-sensitive analysis" ,讨论 Checker 框架如何表明纯度或无副作用。 @SideEffectFree 和 @Pure 注释目前是全有或全无。

您关于部分纯度注释的建议将很有用:它将使 Checker 框架更具表现力，并减少抑制警告的需要，正如当前所要求的那样。 (另一方面，这也是用户需要学习的另一件事；总是存在表达性与复杂性的权衡。)我建议您向 Checker Framework 开发人员建议此功能。