How to tell Checker Framework a null check is inside another method?

I am trying to adopt the checker framework (v 3.18.1) over an existing codebase that used to have the older jsr305 annotations, and coming across some situations that are hard to resolve just by reading the manual (at least for me).

At the moment I am trying to tell the nullness checker that another method contains a null-check that guards the value in question.

I put together this example that shows the issue I am having, a checker error at {*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
    
}

}

Note: i've tried adding 'this.' to those expressions, but it didnt make a difference.

I'd like to get rid of the error at {*1}, however i'd prefer to avoid a castNonNull() call, even if I copy the code to my own project as suggested. Instead I don't mind changing around some of the internal code of methods if need be (like the attempt in the getException2ndVariety() implementation), but I'm hoping this pattern can be expressed with annotations and not a runtime assertions.

Any suggestions much appreciated.

Solution

You almost had it right. You wrote @EnsuresNonNull on method hasException(), but you should have written @EnsuresNonNullIf. getException() does not evaluate to a non-null value every time hasException() is called, but only when hasException() returns true.

You also need to annotate getException() as @Pure. Otherwise, the Nullness Checker will conservatively assume that it might return a different value each time it is called.

Note that you can only write @EnsuresNonNullIf on methods that return boolean, so two uses of it in your code are illegal.

Here is a slight variant of your code that type-checks using the 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;
  }
}