如何告知Checker Framework空值校验逻辑位于另一方法内

修正后可通过空值检查的完整代码 #

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

class Scratch {

    static class Holder {
        @Nullable Exception exception;

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

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

        public @Nullable Exception getException2ndVariety() {
            if (hasException()) return exception;
            return null;
        }

        // 核心修改：替换错误注解
        @EnsuresNonNullIf(expression = "exception", result = true)
        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();
    }
}

修改逻辑说明 #

• 你之前给hasException()用的@EnsuresNonNull注解语义是方法执行完成后，无论返回值是什么，指定的表达式都非空，通常用于修改字段的void方法，和你的方法逻辑完全不匹配，所以不会生效。替换为@EnsuresNonNullIf后，语义匹配：当方法返回true时，exception字段一定非空，空值检查器进入if分支后会自动识别这个后置条件。
• @EnsuresNonNullIf注解仅支持标注返回boolean类型的方法，你给返回Exception类型的getException2ndVariety()加这个注解，自然会触发表达式解析错误，删掉这个错误注解即可。

可选优化 #

如果你需要进一步把getException()的返回值非空性和字段绑定，可以给它补充对应注解：

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

这样如果你直接判断if (holder.getException() != null)，后续使用该返回值也不会触发空值报错。

内容的提问来源于stack exchange，提问作者llaith