0

我正在使用 Java 8 试用Checker Framework的 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 Framework 一个方法不会修改除了它被调用的对象之外的任何对象？因为map.put不调用setX方法，所以 的值x不会改变。

为了摆脱警告，我可以将调用方法更改为：

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

现在没有任何警告。这也是有道理的：不能从外部访问局部变量。但我不喜欢仅仅为了消除警告而引入这个局部变量。

或者，我可以x通过@MonotonicNonNull. 但在我的实际用例中，我想保留将字段设置为空的可能性。

提前致谢！

4

1 回答 1

1

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

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

有什么方法可以告诉 Checker Framework 一个方法不会修改除了它被调用的对象之外的任何对象？

不幸的是，Checker 框架目前没有这个功能。 手册第 21.4.3 节“副作用、确定性、纯度和流量敏感分析”讨论了 Checker 框架如何指示纯度或无副作用。@SideEffectFree 和 @Pure 注释目前是全有或全无。

您对部分纯度注释的建议会很有用：它将使 Checker Framework 更具表现力，并减少抑制警告的需要，正如目前所要求的那样。（另一方面，这也是用户要学习的另一件事；总是要在表现力和复杂性之间进行权衡。）我建议您向 Checker Framework 开发人员提出此功能。

于 2014-10-16T07:02:32.087 回答