@ThrowsException annotation for methods that always throw an exception

This is a feature request for a @ThrowsException method annotation, which indicates that the annotated method throws an exception.
This would be analogous to @TerminatesExecution, in that it would improve the dataflow analysis (flow-sensitive type refinement).

The original suggestion follows.

In my project at work, I encountered this line, which throws an exception:

BusinessException.builder()
        .detail(detailedMessage)
        .transitionFrom(ShippingState.RECEIVED)
        .withIdentifier(ProductSourceIdentifier.WAREHOUSE_ID, warehouseId)
        .buildAndThrow();

Should the Nullness Checker encounter this, it has no way of knowing that an exception is guaranteed to be thrown on this line. Granted, I would have written it like this:

throw BusinessException.builder()
        .detail(detailedMessage)
        .transitionFrom(ShippingState.RECEIVED)
        .withIdentifier(ProductSourceIdentifier.WAREHOUSE_ID, warehouseId)
        .build();

But I didn't write this code, and this is done all over the project.

Now suppose the Nullness Checker encountered something like this:

public ConnectionSource getConnection() {
  if (connectionSource == null) {
    BusinessException.builder()
        .doWhateverStuffIsNeeded()
        .buildAndThrow();
  }
  return connectionSource;
}

It would have no way of knowing that an exception gets thrown when connectionSource is null, so it would issue an error, believing that connectionSource could be null.

In principle, this could be handled by an annotation on the buildAndThrow() method that says that it throws an exception, under a condition. So let's imagine there's an annotation @Throws(String expression) where it declares it will throw an exception if the expression is true. (This is similar to the JetBrains @Contract annotation, which covers the same problem.) Then we could declare the method like this:

@Throws("true")
public void buildAndThrow() { ... }

Now the Nullness Checker would have the information it needs. It would know that an exception is always thrown when connectionSource is null, so would process the method correctly.

The Nullness Checker would be more useful with a facility like this. The preconditions and post conditions are useful, but they don't cover a case like this.

(Please don't suggest that @RequiresNonNull(connectionSource) would solve this problem. In this simplified version, it will, but the actual case was far more complicated, with several method parameters and various tests. In the real-world example where I found this, the only solution that makes sense would be to tell the checker that the buildAndThrow method will throw an exception.)

No implementation files or tests are named. Start by reading the referenced @TerminatesExecution annotation and the Nullness Checker’s flow-sensitive dataflow analysis; done would include a defined @ThrowsException design and checker behavior for methods that always throw.