1

我正在尝试在现有代码库上采用检查器框架（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
    
}

}

注意：我试过添加“这个”。对那些表达，但它没有任何区别。

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

任何建议都非常感谢。

4

1 回答 1

0

你几乎是对的。你写@EnsuresNonNull了方法hasException()，但你应该写@EnsuresNonNullIf。 每次调用时都不会计算为非空值，但仅在返回getException()时才计算。hasException()hasException()true

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

请注意，您只能编写@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;
  }
}
于 2021-11-02T22:38:54.643 回答