如何告诉 Checker Framework 空检查在另一个方法中？

Question

我正在尝试在现有的代码库上采用检查器框架 (v 3.18.1)，该代码库曾经具有较旧的 jsr305 注释，并且遇到了一些仅通过阅读手册很难解决的情况（至少对我来说）。

目前我正试图告诉空值检查器另一个方法包含一个空值检查来保护所讨论的值。

我把这个例子放在一起，显示了我遇到的问题，在 {*1}:

处出现检查错误

class Scratch {

static class Holder {
    @Nullable Exception exception;

    public Holder(@Nullable Exception exception) {
        this.exception = exception;
    }

    @EnsuresNonNullIf(expression = "exception", result = true) // does nothing
    public @Nullable Exception getException() {
        return this.exception;
    }

    @EnsuresNonNullIf(expression = "hasException()", result = true) // fails with parse error
    public @Nullable Exception getException2ndVariety() {
        if (hasException()) return exception;
        return null;
    }

    @EnsuresNonNull("exception") // does nothing
    public boolean hasException() {
        return exception != null;
    }
}

public static void main(String[] args) throws Exception {
    
    Holder holder = new Holder(new Exception());
    
    if (holder.hasException()) throw holder.getException(); // {*1} throwing nullable error
    
}

}

注意：我已经尝试将 'this.' 添加到这些表达式中，但没有任何区别。

我想消除 {*1} 处的错误，但我更愿意避免调用 castNonNull()，即使我按照建议将代码复制到我自己的项目中也是如此。相反，如果需要的话，我不介意改变一些方法的内部代码（比如 getException2ndVariety() 实现中的尝试），但我希望这种模式可以用注释而不是运行时断言来表达。

非常感谢任何建议。

Answer 1

你几乎是对的。你写了 @EnsuresNonNull on method hasException(), but you should have written @EnsuresNonNullIf。 getException() 不会在每次 调用 hasException() 时计算为非空值 ，但仅当 hasException() returns true.

您还需要将 getException() 注释为 @Pure。否则，Nullness Checker 将保守地假设它可能 return 每次调用时都有不同的值。

请注意，您只能在 return 布尔值的方法上编写 @EnsuresNonNullIf，因此在您的代码中两次使用它是非法的。

这里是您的代码的一个小变体，它使用 Nullness Checker 进行类型检查。

import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
import org.checkerframework.checker.nullness.qual.Nullable;

class Scratch {

  public static void main(String[] args) throws Exception {

    Holder holder = new Holder(new Exception());

    if (holder.hasException()) {
      throw holder.getException();
    }
  }
}

class Holder {
  @Nullable Exception exception;

  public Holder(@Nullable Exception exception) {
    this.exception = exception;
  }

  @Pure
  public @Nullable Exception getException() {
    return this.exception;
  }

  @EnsuresNonNullIf(expression = {"getException()"}, result = true)
  public boolean hasException() {
    return getException() != null;
  }
}